isEmbedding_prodMap — Mathlib

English

If f and g are embeddings, then the product map prod.map f g is an embedding.

Русский

Если f и g являются вложениями, то произведение prod.map f g — вложение.

LaTeX

$$$\\text{IsEmbedding}(\\mathrm{Limits.prod.map} f g)$$$

Lean4

theorem isEmbedding_prodMap {W X Y Z : TopCat.{u}} {f : W ⟶ X} {g : Y ⟶ Z} (hf : IsEmbedding f) (hg : IsEmbedding g) :
    IsEmbedding (Limits.prod.map f g) :=
  ⟨isInducing_prodMap hf.isInducing hg.isInducing,
    by
    haveI := (TopCat.mono_iff_injective _).mpr hf.injective
    haveI := (TopCat.mono_iff_injective _).mpr hg.injective
    exact (TopCat.mono_iff_injective _).mp inferInstance⟩

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