isCompact_biUnion — Mathlib

English

If s is a finite set of indices and each f i is compact, then ⋃ i∈s f_i is compact.

Русский

Если s — конечный набор индексов и каждый f_i компактен, то объединение ⋃_{i∈s} f_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 : Set ι} {f : ι → Set X} (hs : s.Finite) (hf : ∀ i ∈ s, IsCompact (f i)) :
    IsCompact (⋃ i ∈ s, f i) :=
  isCompact_iff_ultrafilter_le_nhds'.2 fun l hl =>
    by
    rw [Ultrafilter.finite_biUnion_mem_iff hs] at hl
    rcases hl with ⟨i, his, hi⟩
    rcases (hf i his).ultrafilter_le_nhds _ (le_principal_iff.2 hi) with ⟨x, hxi, hlx⟩
    exact ⟨x, mem_iUnion₂.2 ⟨i, his, hxi⟩, hlx⟩

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