English
Preimages of compact closed sets are compact under a cocompact map when the codomain is Hausdorff.
Русский
Обратные образы компактных замкнутых множеств остаются компактными при когомпактированной карте, если кодом пространства Хаусдорфово.
LaTeX
$$$IsCompact (f^{-1}(s)) \\text{ if } IsCompact s \\text{ and } IsClosed s$$$
Lean4
/-- Preimages of compact closed sets are compact under a cocompact continuous map. -/
theorem isCompact_preimage_of_isClosed (f : CocompactMap α β) ⦃s : Set β⦄ (hs : IsCompact s) (h's : IsClosed s) :
IsCompact (f ⁻¹' s) :=
by
obtain ⟨t, ht, hts⟩ :=
mem_cocompact'.mp
(by
simpa only [preimage_image_preimage, preimage_compl] using
mem_map.mp
(cocompact_tendsto f <| mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩))
exact ht.of_isClosed_subset (h's.preimage <| map_continuous f) (by simpa using hts)
