isClosedEmbedding_comap_of_surjective

English

If f is surjective, then comap f is a closed embedding.

Русский

Если f сюрьективен, то comap f является замкнутым вложением.

LaTeX

$$IsClosedEmbedding (comap f)$$

Lean4

theorem isClosedEmbedding_comap_of_surjective (hf : Surjective f) : IsClosedEmbedding (comap f)
    where
  toIsInducing := comap_isInducing_of_surjective S f hf
  injective := comap_injective_of_surjective f hf
  isClosed_range := isClosed_range_comap_of_surjective S f hf

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