inr_comp_binaryCoproductIso_hom_apply

English

Equating the inr component of the image under binaryCoproductIso.hom with inr x.

Русский

Сравнение второй компоненты образа через бинарный копроизведение и inr.

LaTeX

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

Lean4

@[simp]
theorem inr_comp_binaryCoproductIso_hom_apply (a : C) (x : G.obj a) :
    (binaryCoproductIso F G).hom.app a ((Limits.coprod.inr (X := F)).app a x) = .inr x :=
  congr_fun (congr_app (inr_comp_binaryCoproductIso_hom F G) a) x

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