prodIsoProd_inv_fst — Mathlib

English

The inverse map composed with the first projection equals the canonical first projection map prodFst.

Русский

Обратная карта вместе с первой проекцией даёт каноническую первую проекцию prodFst.

LaTeX

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

Lean4

@[reassoc (attr := simp), elementwise]
theorem prodIsoProd_inv_fst (X Y : TopCat.{u}) : (prodIsoProd X Y).inv ≫ Limits.prod.fst = prodFst := by
  simp [Iso.inv_comp_eq]

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