prodLeftIsoPullback_inv_fst — Mathlib

English

Equality of the inverse-left-projection composition with the fst projection on Y side, expressed via the pullback structure.

Русский

Равенство композиции обратного левого отображения с проекцией fst на стороне Y внутри структуры pullback.

LaTeX

$$$$ (\mathrm{prodLeftIsoPullback}\, Y\, Z)^{\mathrm{inv}} \circ \mathrm{prod.fst} \; (X := Y).\mathrm{left} = \mathrm{pullback.fst}\; Y.hom \; Z.hom $$$$

Lean4

@[reassoc (attr := simp)]
theorem prodLeftIsoPullback_inv_fst : (prodLeftIsoPullback Y Z).inv ≫ (prod.fst (X := Y)).left = pullback.fst _ _ :=
  IsPullback.isoPullback_inv_fst _

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