inr_pushoutZeroZeroIso_hom — Mathlib

English

The composition pushout.inr followed by the hom part of the pushoutZeroZeroIso equals coprod.inr.

Русский

Сложение pushout.inr затем компонент hom изоморфизма pushoutZeroZeroIso равно coprod.inr.

LaTeX

$$$$\text{pushout.inr} \;\circ\; (\text{pushoutZeroZeroIso } X Y).\mathrm{hom} = \mathrm{coprod.inr}. $$$$

Lean4

@[simp]
theorem inr_pushoutZeroZeroIso_hom (X Y : C) [HasBinaryCoproduct X Y] :
    pushout.inr _ _ ≫ (pushoutZeroZeroIso X Y).hom = coprod.inr :=
  by
  dsimp [pushoutZeroZeroIso]
  simp

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