English
Let X be a topological space and {f_i} a finite family of subsets of X such that each f_i is both open and closed. Then the union over i in the finite index set is also open and closed.
Русский
Пусть X — топологическое пространство и {f_i} конечная семейство подмножеств X, каждое из которых одновременно открыто и замкнуто. Тогда объединение по всем i из конечного множества также открыто и замкнуто.
LaTeX
$$$ \\left( \\forall i \\in s,\\ IsClopen(f(i)) \\right) \\Rightarrow IsClopen\\left(\\bigcup_{i \\in s} f(i)\\right) $$$
Lean4
theorem isClopen_biUnion_finset {Y} {s : Finset Y} {f : Y → Set X} (h : ∀ i ∈ s, IsClopen <| f i) :
IsClopen (⋃ i ∈ s, f i) :=
s.finite_toSet.isClopen_biUnion h
