English
If s is compact and {c_i} (i in b) is a family of open sets covering s, then there exists a finite subfamily that still covers s: there exists b' ⊆ b finite with s ⊆ ⋃_{i∈b'} c_i.
Русский
Если s компактно и {c_i} (для i в b) образует семейство открытых множеств, покрывающее s, то существует конечное подпокрытие: найдётся b' ⊆ b конечное такое, что s ⊆ ⋃_{i∈b'} c_i.
LaTeX
$$$\\text{If } s \\text{ is compact and } (c_i)_{i \\in b} \\text{ open with } s \\subseteq \\bigcup_{i\\in b} c_i, \\text{ then } \\exists\, b'\\subseteq b,\\; b' \\text{ finite and } s \\subseteq \\bigcup_{i\\in b'} c_i.$$$
Lean4
/-- For every open cover of a compact set, there exists a finite subcover. -/
theorem elim_finite_subcover_image {b : Set ι} {c : ι → Set X} (hs : IsCompact s) (hc₁ : ∀ i ∈ b, IsOpen (c i))
(hc₂ : s ⊆ ⋃ i ∈ b, c i) : ∃ b', b' ⊆ b ∧ Set.Finite b' ∧ s ⊆ ⋃ i ∈ b', c i :=
by
simp only [Subtype.forall', biUnion_eq_iUnion] at hc₁ hc₂
rcases hs.elim_finite_subcover (fun i => c i : b → Set X) hc₁ hc₂ with ⟨d, hd⟩
refine ⟨Subtype.val '' d.toSet, ?_, d.finite_toSet.image _, ?_⟩
· simp
· rwa [biUnion_image]
