inr_isoIsPushout_inv — Mathlib

English

If h is a pushout and h' is another pushout, then the right leg satisfies: inr' ≫ (h.isoIsPushout _ _ h').inv = inr.

Русский

Если h и h' — пушауты, то правая ножка удовлетворяет: inr' ≫ (h.isoIsPushout _ _ h').inv = inr.

LaTeX

$$$\forall h,h' : IsPushout\ f\ g\ inl\ inr,\ inl' , inr' : IsPushout\ f\ g\ inl'\ inr' : inr' ≫ (h.isoIsPushout _ _ h').inv = inr$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_isoIsPushout_inv (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') :
    inr' ≫ (h.isoIsPushout _ _ h').inv = inr := by simp only [Iso.comp_inv_eq, inr_isoIsPushout_hom]

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