prodLeftIsoPullback_hom_fst — Mathlib

English

The inverse of the left projection through the pullback interacts with the product’s fst projection to give a canonical equality.

Русский

Обратная левая проекция через pullback взаимодействует с проекцией fst произведения, порождая каноническое равенство.

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_hom_fst : (prodLeftIsoPullback Y Z).hom ≫ pullback.fst _ _ = (prod.fst (X := Y)).left :=
  IsPullback.isoPullback_hom_fst _

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