English
For a compact set s and a finite open cover {U_i}, there exist compact K_i ⊆ U_i such that s = ⋃ K_i.
Русский
Для компактного множества s и конечного открытого покрытия {U_i} существуют компактные K_i ⊆ U_i такие, что s = ⋃ K_i.
LaTeX
$$∃ K : ι → Set X, (∀ i, IsCompact(K i)) ∧ (∀ i, K i ⊆ U i) ∧ s = ⋃ i∈t, K i$$
Lean4
/-- For every finite open cover `Uᵢ` of a compact set, there exists a compact cover `Kᵢ ⊆ Uᵢ`. -/
theorem finite_compact_cover {s : Set X} (hs : IsCompact s) {ι : Type*} (t : Finset ι) (U : ι → Set X)
(hU : ∀ i ∈ t, IsOpen (U i)) (hsC : s ⊆ ⋃ i ∈ t, U i) :
∃ K : ι → Set X, (∀ i, IsCompact (K i)) ∧ (∀ i, K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i := by
classical
induction t using Finset.induction generalizing U s with
| empty =>
refine ⟨fun _ => ∅, fun _ => isCompact_empty, fun i => empty_subset _, ?_⟩
simpa only [subset_empty_iff, Finset.notMem_empty, iUnion_false, iUnion_empty] using hsC
| insert x t hx ih =>
simp only [Finset.set_biUnion_insert] at hsC
simp only [Finset.forall_mem_insert] at hU
have hU' : ∀ i ∈ t, IsOpen (U i) := fun i hi => hU.2 i hi
rcases hs.binary_compact_cover hU.1 (isOpen_biUnion hU') hsC with ⟨K₁, K₂, h1K₁, h1K₂, h2K₁, h2K₂, hK⟩
rcases ih h1K₂ U hU' h2K₂ with ⟨K, h1K, h2K, h3K⟩
refine ⟨update K x K₁, ?_, ?_, ?_⟩
· intro i
rcases eq_or_ne i x with rfl | hi
· simp only [update_self, h1K₁]
· simp only [update_of_ne hi, h1K]
· intro i
rcases eq_or_ne i x with rfl | hi
· simp only [update_self, h2K₁]
· simp only [update_of_ne hi, h2K]
· simp only [Finset.set_biUnion_insert_update _ hx, hK, h3K]
