inl_comp_binaryCoproductIso_hom — Mathlib

English

The left injection into a coproduct, followed by the left component of the binary coproduct iso, equals the canonical left injection.

Русский

Левая инъекция в копроизведение, затем левая компонента двоичного копроизведения, совпадают с канонической инъекцией слева.

LaTeX

$$$ \mathrm{Limits.coprod.inl} \;\gg\; (binaryCoproductIso F G).hom = \mathrm{coprod.inl} $$$

Lean4

@[simp]
theorem inl_comp_binaryCoproductIso_hom : Limits.coprod.inl ≫ (binaryCoproductIso F G).hom = coprod.inl :=
  by
  simp only [binaryCoproductIso]
  aesop

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