isClosed_iUnion_of_finite — Mathlib

English

If s is finite and every s(i) is closed, then the union ⋃ i, s(i) is closed.

Русский

Если s ограничено (конечное) и каждое s(i) замкнуто, то ⋃ i, s(i) замкнуто.

LaTeX

$$$(\forall i, \operatorname{IsClosed}(s(i))) \Rightarrow \operatorname{IsClosed}(\bigcup_i s(i))$$$

Lean4

theorem isClosed_iUnion_of_finite [Finite ι] {s : ι → Set X} (h : ∀ i, IsClosed (s i)) : IsClosed (⋃ i, s i) :=
  by
  simp only [← isOpen_compl_iff, compl_iUnion] at *
  exact isOpen_iInter_of_finite h

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