isClopen_iUnion_of_finite — Mathlib

English

The union over a finite index set of clopen sets is clopen.

Русский

Объединение по конечному числу индексов множества, состоящих из открыто-замкнутых множеств, есть открыто-замкнутое.

LaTeX

$$$\forall Y\ [Finite dot Y]\ {s:\ Y \to Set X},\ (\forall i, IsClopen(s(i))) \Rightarrow IsClopen(\bigcup_i s(i))$$$

Lean4

theorem isClopen_iUnion_of_finite {Y} [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : IsClopen (⋃ i, s i) :=
  ⟨isClosed_iUnion_of_finite (forall_and.1 h).1, isOpen_iUnion (forall_and.1 h).2⟩

Похожие утверждения