no goals
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : RegularSpace α
a✝ : α
s✝ : Set α
B : Set (Set α)
hB : IsTopologicalBasis B
a : α
s : Set α
h : s ∈ 𝓝 a
⊢ ∃ t, t ∈ B ∧ a ∈ t ∧ closure t ⊆ s
simpa only [exists_prop, and_assoc] using hB.nhds_hasBasis.nhds_closure.mem_iff.mp h