inl_isoPushout_hom — Mathlib

English

If h is a pushout of f,g with inl,inr and HasPushout f g, then inl ≫ h.isoPushout.hom = pushout.inl f g and inr ≫ h.isoPushout.hom = pushout.inr f g.

Русский

Левая и правая ножки пушаута согласованы с инъекциями копродукта: inl ≫ hom = pushout.inl и inr ≫ hom = pushout.inr.

LaTeX

$$$inl \gg g = pushout.inl\ f\ g$ и $inr \gg h = pushout.inr\ f\ g$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_isoPushout_hom (h : IsPushout f g inl inr) [HasPushout f g] : inl ≫ h.isoPushout.hom = pushout.inl _ _ := by
  simp [← Iso.eq_comp_inv]

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