isClopen_iInter_of_finite — Mathlib

English

If {s_i} is a finite family of sets in X and each s_i is clopen, then their intersection over i in the finite index set is closed and open (clopen).

Русский

Если {s_i} — конечное семейство множеств в X, и каждое s_i является как открытым, так и замкнутым, то их пересечение по всем i также открыто и замкнуто.

LaTeX

$$$ (\\forall i \\in s,\\ IsClopen(s_i)) \\Rightarrow IsClopen\\left(\\bigcap_{i \\in s} s_i\\right) $$$

Lean4

theorem isClopen_iInter_of_finite {Y} [Finite Y] {s : Y → Set X} (h : ∀ i, IsClopen (s i)) : IsClopen (⋂ i, s i) :=
  ⟨isClosed_iInter (forall_and.1 h).1, isOpen_iInter_of_finite (forall_and.1 h).2⟩

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