inl_isoIsPushout_inv — Mathlib

English

If h is a pushout of f,g with inl,inr and h' is another pushout, then the left leg of the pushout iso has inverse relation: inl' ≫ (h.isoIsPushout _ _ h').inv = inl.

Русский

Если h и h' — пушауты, то левая нога изоморфизма пушаута удовлетворяет: inl' ≫ (h.isoIsPushout _ _ h').inv = inl.

LaTeX

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

Lean4

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

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