pullbackIsoProdSubtype_hom_fst — Mathlib

English

The forward projection map of the canonical isomorphism from the pullback to the product satisfies that composing it with pullbackFst equals the usual fst map.

Русский

Переходная проекция канонического изоморфизма от пределa к произведению удовлетворяет свойству: композиция с pullbackFst даёт обычную fst.

LaTeX

$$$ (pullbackIsoProdSubtype f g).hom \circ pullbackFst\, f\, g = pullback.fst\, f\, g $$$

Lean4

theorem pullbackIsoProdSubtype_hom_fst (f : X ⟶ Z) (g : Y ⟶ Z) :
    (pullbackIsoProdSubtype f g).hom ≫ pullbackFst f g = pullback.fst _ _ := by
  rw [← Iso.eq_inv_comp, pullbackIsoProdSubtype_inv_fst]

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