no goals
α : Type u_1
β : Type ?u.6768
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ∈ 𝓝ˢ t ↔ ∀ (x : α), x ∈ t → s ∈ 𝓝 x
simp_rw [nhdsSet, Filter.mem_sSup, ball_image_iff]