no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s U : Set α
h : U ∈ ⨆ (x : α) (_ : x ∈ s), 𝓝 x
⊢ ∀ (x : α), x ∈ s → U ∈ 𝓝 x
simpa using h