inr_comp_pushoutObjIso_inv — Mathlib

English

Likewise for the right injection, the inverse of the pushoutObjIso composed with the right injection recovers the right injection of the components.

Русский

Аналогично для inr: inv ∘ pushoutObjIso восстанавливает inr на компонентах.

LaTeX

$$$ (pushout.inr\\, f\\, g).app\\, d \\;\\circ\\; (pushoutObjIso\\, f\\, g\\, d).inv = pushout.inr\$ f.{\\rm app}\\, d\$\$ g.{\\rm app}\\, d\$ $$$

Lean4

@[reassoc (attr := simp)]
theorem inr_comp_pushoutObjIso_inv (f : F ⟶ G) (g : F ⟶ H) (d : D) :
    pushout.inr (f.app d) (g.app d) ≫ (pushoutObjIso f g d).inv = (pushout.inr f g).app d := by simp [pushoutObjIso]

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