inl_comp_pushoutObjIso_inv — Mathlib

English

In the pushout setting, the inverse of the pushoutObjIso composed with the left injection equals the left injection of the components.

Русский

В контексте pushout обратная сторона от pushoutObjIso, композиция с inl, равна inl на компонентах.

LaTeX

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

Lean4

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

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