prodIsoProd_hom_fst — Mathlib

English

The forward map of the prodIsoProd is compatible with the first projection: (prodIsoProd X Y).hom ∘ prodFst = Limits.prod.fst.

Русский

Гомоморфизм (prodIsoProd X Y).hom совместим с первой проекцией: (prodIsoProd X Y).hom ∘ prodFst = Limits.prod.fst.

LaTeX

$$$(\\mathrm{prodIsoProd}(X,Y)).hom \\circ \\mathrm{prodFst} = \\mathrm{Limits.prod.fst}$$$

Lean4

@[reassoc (attr := simp)]
theorem prodIsoProd_hom_fst (X Y : TopCat.{u}) : (prodIsoProd X Y).hom ≫ prodFst = Limits.prod.fst :=
  by
  simp [← Iso.eq_inv_comp, prodIsoProd]
  rfl

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