inl_pushoutZeroZeroIso_inv — Mathlib

English

The composition coprod.inl with the inverse of pushoutZeroZeroIso equals the pushout.inl for the zero case.

Русский

Сложение coprod.inl с обратным изоморфизмом pushoutZeroZeroIso даёт pushout.inl в нулевом случае.

LaTeX

$$$$ \mathrm{coprod.inl} \circ (\text{pushoutZeroZeroIso } X Y)^{-1} = \mathrm{pushout.inl}_{0 0}. $$$$

Lean4

@[simp]
theorem inl_pushoutZeroZeroIso_inv (X Y : C) [HasBinaryCoproduct X Y] :
    coprod.inl ≫ (pushoutZeroZeroIso X Y).inv = pushout.inl _ _ := by simp [Iso.comp_inv_eq]

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