isCompact_sUnion — Mathlib

English

If S is finite and every member is compact, then the union ⋃ S is compact.

Русский

Если множество S конечно и каждый элемент компактен, то их объединение компактно.

LaTeX

$$$S\\text{ finite} \\rightarrow (\\forall s \\in S, IsCompact s) \\rightarrow IsCompact (\\\\bigcup S)$$$

Lean4

theorem isCompact_sUnion {S : Set (Set X)} (hf : S.Finite) (hc : ∀ s ∈ S, IsCompact s) : IsCompact (⋃₀ S) := by
  rw [sUnion_eq_biUnion]; exact hf.isCompact_biUnion hc

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