snd_isEmbedding_of_left — Mathlib

English

If f is an embedding, then for any g the pullback.snd f g is an embedding.

Русский

Если f — вложение, то для любого g предел pullback.snd f g является вложением.

LaTeX

$$$ \text{IsEmbedding}\big( \mathrm{pullback.snd} f g \big) $$$

Lean4

theorem snd_isEmbedding_of_left {X Y S : TopCat} {f : X ⟶ S} (H : IsEmbedding f) (g : Y ⟶ S) :
    IsEmbedding <| ⇑(pullback.snd f g) :=
  by
  convert
    (homeoOfIso (asIso (pullback.snd (𝟙 S) g))).isEmbedding.comp
      (pullback_map_isEmbedding (i₂ := 𝟙 Y) f g (𝟙 S) g H (homeoOfIso (Iso.refl _)).isEmbedding (𝟙 _) rfl (by simp))
  simp [homeoOfIso, ← coe_comp]

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