no goals
𝓕 : Type ?u.494104
𝕜 : Type ?u.494107
α : Type ?u.494110
ι : Type ?u.494113
κ : Type ?u.494116
E : Type u_1
F : Type ?u.494122
G : Type ?u.494125
inst✝² : SeminormedGroup E
inst✝¹ : SeminormedGroup F
inst✝ : SeminormedGroup G
s : Set E
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
⊢ a ∈ closure s ↔ ∀ (ε : ℝ), 0 < ε → ∃ b, b ∈ s ∧ ‖a / b‖ < ε
simp [Metric.mem_closure_iff, dist_eq_norm_div]