isCompact_biUnion — Mathlib

English

For a finite index set and compact sets f i, the union over i is compact.

Русский

Для конечного множества индексов и компактных множеств f_i их объединение по i компактно.

LaTeX

$$$s\\text{ finite} \\Rightarrow (\\\\forall i \\in s, IsCompact (f i)) \\Rightarrow IsCompact (\\\\bigcup_{i \\in s} f i)$$$

Lean4

theorem isCompact_biUnion (s : Finset ι) {f : ι → Set X} (hf : ∀ i ∈ s, IsCompact (f i)) : IsCompact (⋃ i ∈ s, f i) :=
  s.finite_toSet.isCompact_biUnion hf

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