English
IsCompact s if and only if every open cover of s has a finite subcover.
Русский
Классическая эквивалентность: компактность s равносильна тому, что любой открытый покров s имеет конечное подпокрытие.
LaTeX
$$$IsCompact\\,s \\iff (\\forall \\mathcal U: \\text{ι} \\to Set X, \\; (\\forall i, IsOpen(\\mathcal U_i)) \\to (s \\subseteq \\bigcup_i \\mathcal U_i) \\to \\exists t : Finset ι,\\ s \\subseteq \\bigcup_{i \\in t} \\mathcal U_i)$$$
Lean4
/-- A set `s` is compact if and only if
for every family of closed sets whose intersection avoids `s`,
there exists a finite subfamily whose intersection avoids `s`. -/
theorem isCompact_iff_finite_subfamily_closed :
IsCompact s ↔
∀ {ι : Type u} (t : ι → Set X),
(∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ → ∃ u : Finset ι, (s ∩ ⋂ i ∈ u, t i) = ∅ :=
⟨fun hs => hs.elim_finite_subfamily_closed, isCompact_of_finite_subfamily_closed⟩
