inr_comp_binaryCoproductIso_hom — Mathlib

English

Applying binaryCoproductIso.hom to coprod.inr yields the inr embedding of x.

Русский

Применение бинарного копроизведения к inr возвращает inr x.

LaTeX

$$$\text{binaryCoproductIso}_{{F,G}}\,\mathrm{hom}.app a (\mathrm{coprod.inr.app a} x) = \mathrm{inr} x$$$

Lean4

@[simp]
theorem inr_comp_binaryCoproductIso_hom : Limits.coprod.inr ≫ (binaryCoproductIso F G).hom = coprod.inr :=
  by
  simp [binaryCoproductIso]
  aesop

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