no goals
α : Type u
β : Type v
X : Type ?u.96096
ι : Type ?u.96099
inst✝ : PseudoMetricSpace α
x y z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ ε, ε > 0 ∧ ball x ε ⊆ s
simp only [isOpen_iff_mem_nhds, mem_nhds_iff]