English
If f is a closed embedding, the complement of range f is compact, and s is retrocompact, then f^{-1}(s) is retrocompact.
Русский
Если f — замкнутое вложение, компактен комплемент образа range f, и s ретрокомпактно, то предобраз f^{-1}(s) ретрокомпактно.
LaTeX
$$IsClosedEmbedding f → IsCompact (range f)ᶜ → IsRetrocompact s → IsRetrocompact (f^{-1} s)$$
Lean4
@[stacks 09YE "Extracted from the proof"]
theorem preimage_of_isClosedEmbedding {s : Set Y} (hf : IsClosedEmbedding f) (hf' : IsCompact (range f)ᶜ)
(hs : IsRetrocompact s) : IsRetrocompact (f ⁻¹' s) :=
by
rintro U hUcomp hUopen
have hfUopen : IsOpen (f '' U ∪ (range f)ᶜ) := by
simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm] using
(hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
have hfUcomp : IsCompact (f '' U ∪ (range f)ᶜ) := (hUcomp.image hf.continuous).union hf'
simpa [inter_union_distrib_left, inter_left_comm, inter_eq_right.2 (image_subset_range ..), hf.isCompact_iff,
image_preimage_inter] using (hs hfUcomp hfUopen).inter_left hf.isClosed_range
