English
IsCompactOpenCovered f U is equivalent to the sigmaMk-form of the same covering property; the two formulations are interchangeable under appropriate encoding.
Русский
Свойство покрывающего множества компактно-открытым способом эквивалентно сигма-представлению этого свойства; две формулировки эквивалентны при соответствующем кодировании.
LaTeX
$$$IsCompactOpenCovered f U \iff IsCompactOpenCovered (fun (x:Unit) (p:\Sigma i:ι, X i) => f p.1 p.2) U.$$$
Lean4
theorem of_isOpenMap [TopologicalSpace S] [∀ i, PrespectralSpace (X i)] (hfc : ∀ i, Continuous (f i))
(h : ∀ i, IsOpenMap (f i)) {U : Set S} (hs : ∀ x ∈ U, ∃ i y, f i y = x) (hU : IsOpen U) (hc : IsCompact U) :
IsCompactOpenCovered f U := by
rw [iff_isCompactOpenCovered_sigmaMk, iff_of_unique]
refine
(isOpenMap_sigma.mpr h).exists_opens_image_eq_of_prespectralSpace (continuous_sigma_iff.mpr hfc) (fun x hx ↦ ?_) hU
hc
simpa using hs x hx
