no goals
α : Type u
β : Type v
ι : Type ?u.30840
π : ι → Type ?u.30845
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
a : α
f : Filter α
hf : NeBot f
hfa : f ≤ 𝓟 {a}
⊢ 𝓟 {a} ≤ 𝓝 a
simpa only [principal_singleton] using pure_le_nhds a