no goals
α : Type u_1
β : Type ?u.16439
γ : Type ?u.16442
δ : Type ?u.16445
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : Set.Finite S
a : α
⊢ 𝓝[⋃₀ S] a = ⨆ (s : Set α) (_ : s ∈ S), 𝓝[s] a
rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]