no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ IsOpen s ↔ ∀ (x : α), x ∈ s → ∀ (l : Ultrafilter α), ↑l ≤ 𝓝 x → s ∈ l
simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter]