isCompact_iff_finite_subcover — Mathlib

English

If every open cover of s has a finite subcover, then s is compact.

Русский

Если каждый открытый покров s имеет конечное подпокрытие, то s компактно.

LaTeX

$$$\\Big(\\forall\\mathcal U:\\text{ι} \\to Set X,\\; (\\forall i, IsOpen(\\mathcal U_i)) \\rightarrow (s \\subseteq \\bigcup_i \\mathcal U_i) \\rightarrow \\exists t : Finset ι, s \\subseteq \\bigcup_{i \\in t} \\mathcal U_i\\Big) \\Rightarrow IsCompact s$$

Lean4

/-- A set `s` is compact if and only if
for every open cover of `s`, there exists a finite subcover. -/
theorem isCompact_iff_finite_subcover :
    IsCompact s ↔
      ∀ {ι : Type u} (U : ι → Set X), (∀ i, IsOpen (U i)) → (s ⊆ ⋃ i, U i) → ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i :=
  ⟨fun hs => hs.elim_finite_subcover, isCompact_of_finite_subcover⟩

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