isCompact_iUnion — Mathlib

English

If ι is finite and each f_i is compact, then the union over i is compact.

Русский

Если индексное множество ι конечное и каждый f_i компактен, то ⋃ i, f_i компактно.

LaTeX

$$$\\text{Finite } ι \\Rightarrow (\\forall i, IsCompact (f i)) \\Rightarrow IsCompact (\\\\union i, f i)$$$

Lean4

theorem isCompact_iUnion {ι : Sort*} {f : ι → Set X} [Finite ι] (h : ∀ i, IsCompact (f i)) : IsCompact (⋃ i, f i) :=
  (finite_range f).isCompact_sUnion <| forall_mem_range.2 h

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