no goals
𝓕 : Type ?u.330243
𝕜 : Type ?u.330246
α : Type ?u.330249
ι : Type ?u.330252
κ : Type ?u.330255
E : Type u_1
F : Type ?u.330261
G : Type ?u.330264
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r✝ r₁ r₂ : ℝ
r : ℝ≥0∞
⊢ a ∈ EMetric.ball 1 r ↔ ↑‖a‖₊ < r
rw [EMetric.mem_ball, edist_eq_coe_nnnorm']