preimage_of_isOpenEmbedding — Mathlib

English

If f is an open embedding and s is retrocompact, then the preimage f^{-1}(s) is retrocompact.

Русский

Если f — открытое вложение и s ретрокомпактно, то прообраз f^{-1}(s) ретрокомпактно.

LaTeX

$$IsOpenEmbedding f → IsRetrocompact s → IsRetrocompact (f^{-1} s)$$

Lean4

@[stacks 005J "Extracted from the proof"]
theorem preimage_of_isOpenEmbedding {s : Set Y} (hf : IsOpenEmbedding f) (hs : IsRetrocompact s) :
    IsRetrocompact (f ⁻¹' s) := by
  rintro U hUcomp hUopen
  rw [hf.isCompact_iff, image_preimage_inter]
  exact hs (hUcomp.image hf.continuous) <| hf.isOpenMap _ hUopen

Похожие утверждения