fst_opProdIsoCoprod_hom — Mathlib

English

The first op (fst) component of the opProdIsoCoprod is the opposite of the coprod inl.

Русский

Первая компонентa противоположного произведения-копродукта равна противоположности инъекции inl копродукта.

LaTeX

$$prod.fst.op ≫ (opProdIsoCoprod A B).hom = coprod.inl.unop$$

Lean4

@[reassoc (attr := simp)]
theorem fst_opProdIsoCoprod_hom : prod.fst.op ≫ (opProdIsoCoprod A B).hom = coprod.inl := by
  rw [opProdIsoCoprod, ← op_comp, prod.lift_fst, Quiver.Hom.op_unop]

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