English
If S is a finite set of subsets of α, the neighborhood at a with respect to the union ⋃ S equals the supremum over s ∈ S of nhdsWithin a s.
Русский
Если S — конечное множество подмножеств пространства, то окрестность в a относительно ⋃ S равна наибольшему объединению по s ∈ S окрестностей 𝓝[s] a.
LaTeX
$$$$ 𝓝[⋃_{s ∈ S} s] a = \\bigvee_{s ∈ S} 𝓝[s] a $$$$
Lean4
theorem nhdsWithin_sUnion {S : Set (Set α)} (hS : S.Finite) (a : α) : 𝓝[⋃₀ S] a = ⨆ s ∈ S, 𝓝[s] a := by
rw [sUnion_eq_biUnion, nhdsWithin_biUnion hS]