no goals
α : Type u_2
β : Type ?u.16749
γ : Type ?u.16752
δ : Type ?u.16755
inst✝¹ : TopologicalSpace α
ι : Sort u_1
inst✝ : Finite ι
s : ι → Set α
a : α
⊢ 𝓝[⋃ (i : ι), s i] a = ⨆ (i : ι), 𝓝[s i] a
rw [← sUnion_range, nhdsWithin_sUnion (finite_range s), iSup_range]