no goals
𝓕 : Type ?u.463871
𝕜 : Type ?u.463874
α : Type ?u.463877
ι : Type ?u.463880
κ : Type ?u.463883
E : Type u_1
F : Type ?u.463889
G : Type ?u.463892
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
x : E
⊢ x ∈ closure {1} ↔ ‖x‖ = 0
rw [← closedBall_zero', mem_closedBall_one_iff, (norm_nonneg' x).le_iff_eq]