prodLeftIsoPullback_inv_snd — Mathlib

English

Symmetric relation to the fst case for the snd projection.

Русский

Симметричное отношение к случаю fst для проекции snd.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem prodLeftIsoPullback_inv_snd : (prodLeftIsoPullback Y Z).inv ≫ (prod.snd (X := Y)).left = pullback.snd _ _ :=
  IsPullback.isoPullback_inv_snd _

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