English
Let X be a topological space and S a finite set of indices ι with f: ι → Set X. Then closure of the union of the corresponding sets equals the union of their closures: closure (⋃ i ∈ S, f i) = ⋃ i ∈ S, closure (f i).
Русский
Пусть X — топологическое пространство, S — конечный набор индексов ι, и функция f: ι → Set X. Тогда замыкание объединения соответствующих множеств равно объединению их замыканий: closure (⋃ i ∈ S, f i) = ⋃ i ∈ S, closure (f i).
LaTeX
$$$\\\\overline{\\\\bigcup_{i \\\\\\in \\\\mathsf{S}} f(i)} = \\\\bigcup_{i \\\\\\in \\\\mathsf{S}} \\\\overline{f(i)}$$$
Lean4
theorem closure_biUnion {ι : Type*} {s : Set ι} (hs : s.Finite) (f : ι → Set X) :
closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i) := by simp [closure_eq_compl_interior_compl, hs.interior_biInter]
