English
For every open cover of a compact set, there exists a finite subcover.
Русский
Для любого открытого покрытия компактного множества существует конечное подпокрытие.
LaTeX
$$$IsCompact(s) \rightarrow \forall U:\ \iota \to Set X,\ (\forall i, IsOpen(U(i))) \rightarrow s \subseteq \bigcup_i U(i) \rightarrow \exists t : Finset \iota, s \subseteq \bigcup_{i \in t} U(i)$$$
Lean4
/-- For every open cover of a compact set, there exists a finite subcover. -/
theorem elim_finite_subcover {ι : Type v} (hs : IsCompact s) (U : ι → Set X) (hUo : ∀ i, IsOpen (U i))
(hsU : s ⊆ ⋃ i, U i) : ∃ t : Finset ι, s ⊆ ⋃ i ∈ t, U i :=
hs.elim_directed_cover _ (fun _ => isOpen_biUnion fun i _ => hUo i) (iUnion_eq_iUnion_finset U ▸ hsU)
(directed_of_isDirected_le fun _ _ h => biUnion_subset_biUnion_left h)
