α : Type u
β : Type v
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen s → s ∈ f
α : Type u
β : Type v
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ f ≤ (fun t => 𝓝 a) t
rw [le_nhds_iff]
no goals
α : Type u
β : Type v
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen s → s ∈ f
exact ⟨fun H s hs has => H _ has hs, fun H s has hs => H _ hs has⟩