English
There is a canonical isomorphism between the opposite of the product A × B and the coproduct of opposites Aᵒᵖ ⊔ Bᵒᵖ; the inverse, when unop, composed with the left injection unop, equals the left projection fst. In symbols, the inverse leg composed with the left injection is the first projection.
Русский
Существует канонический изоморфизм между противоположностью произведения A × B и копродукта Aᵒᵖ ⊔ Bᵒᵖ; обратная стрелка, взятая через unop и сопоставленная с инжекцией слева, равна левому проекционному гомоморфизму fst.
LaTeX
$$$$(\operatorname{opProdIsoCoprod} A B)^{-1}.unop \;\;\circ \;\; \operatorname{coprod.inl}.unop = \operatorname{prod.fst}.$$$$
Lean4
@[reassoc (attr := simp)]
theorem opProdIsoCoprod_inv_inl : (opProdIsoCoprod A B).inv.unop ≫ coprod.inl.unop = prod.fst := by
rw [← unop_comp, inl_opProdIsoCoprod_inv, Quiver.Hom.unop_op]
