inr_isoIsPushout_hom — Mathlib

English

Symmetrically to the left leg, the right leg respects pushout isomorphisms: inr ≫ (h.isoIsPushout _ _ h').hom = inr'.

Русский

Аналогично левой ножке: правая ножка совместима с изоморфизмом пушаута: inr ≫ (h.isoIsPushout _ _ h').hom = inr'.

LaTeX

$$$\forall h,h' : IsPushout\ f\ g\ inl\ inr,\ inl',inr' : IsPushout\ f\ g\ inl'\ inr'\;:\; inr \;\ggg\; (h.isoIsPushout _ _ h').hom = inr'$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_isoIsPushout_hom (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
    inr ≫ (h.isoIsPushout _ _ h').hom = inr' :=
  IsColimit.comp_coconePointUniqueUpToIso_hom h.isColimit h'.isColimit WalkingSpan.right

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