no goals
α : Type u_1
β : Type ?u.4968
γ : Type ?u.4971
δ : Type ?u.4974
inst✝ : TopologicalSpace α
t : Set α
a : α
s : Set α
⊢ t ∈ 𝓝[s] a ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t
simpa only [and_assoc, and_left_comm] using (nhdsWithin_basis_open a s).mem_iff