image_of_isEmbedding — Mathlib

English

If s is retrocompact in X, f is an embedding, and range f is retrocompact, then the image f''s is retrocompact in Y.

Русский

Если s ретрокомпактно в X, f — вложение, и образ f(X) ретрокомпактен, то изображение f''s ретрокомпактно в Y.

LaTeX

$$IsRetrocompact(s) → IsEmbedding f → IsRetrocompact(range f) → IsRetrocompact(f'' s)$$

Lean4

@[stacks 005B]
theorem image_of_isEmbedding (hs : IsRetrocompact s) (hfemb : IsEmbedding f) (hfcomp : IsRetrocompact (range f)) :
    IsRetrocompact (f '' s) := by
  rintro U hUcomp hUopen
  rw [← image_inter_preimage, ← hfemb.isCompact_iff]
  refine hs ?_ <| hUopen.preimage hfemb.continuous
  rw [hfemb.isCompact_iff, image_preimage_eq_inter_range, inter_comm]
  exact hfcomp hUcomp hUopen

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