snd_opProdIsoCoprod_hom — Mathlib

English

The second op (snd) component of the opProdIsoCoprod equals the opposite of coprod.inr.

Русский

Вторая компонентa противоположного произведения-копродукта эквивалентна противоположности coprod.inr.

LaTeX

$$prod.snd.op ≫ (opProdIsoCoprod A B).hom = coprod.inr.unop$$

Lean4

@[reassoc (attr := simp)]
theorem snd_opProdIsoCoprod_hom : prod.snd.op ≫ (opProdIsoCoprod A B).hom = coprod.inr := by
  rw [opProdIsoCoprod, ← op_comp, prod.lift_snd, Quiver.Hom.op_unop]

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