English
Equality of covering statements transfers under a change of indexing to a sigma-type representation; the IsCompactOpenCovered property is equivalent to the same property for the sigma-skewed index.
Русский
Свойство покрытия компактно-открытым образом сохраняется при переходе к представлению через сигма-теп.
LaTeX
$$$IsCompactOpenCovered f U \iff IsCompactOpenCovered (\lambda x p. f p.fst p.snd) U.$$$
Lean4
theorem of_iUnion_eq_of_finite (s : Set (Set S)) (hs : ⋃ t ∈ s, t = U) (hf : s.Finite)
(H : ∀ t ∈ s, IsCompactOpenCovered f t) : IsCompactOpenCovered f U :=
by
rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique]
have (t) (h : t ∈ s) : ∃ (V : Opens (Σ i, X i)), IsCompact V.1 ∧ (fun p ↦ f p.fst p.snd) '' V.carrier = t :=
by
have := H t h
rwa [iff_isCompactOpenCovered_sigmaMk, iff_of_unique] at this
choose V hVeq hVc using this
refine ⟨⨆ (t : s), V t t.2, ?_, ?_⟩
· simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk]
have : Finite s := hf
exact isCompact_iUnion (fun _ ↦ hVeq _ _)
· simp [Set.image_iUnion, ← hs]
simp_all
