no goals
α : Type u_1
β : Type ?u.13421
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s₁ s₂ t₁ t₂ : Set α
x : α
s t : Set α
⊢ 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t
simp only [nhdsSet, image_union, sSup_union]