binaryProductIso_hom_comp_fst — Mathlib

English

The first projection of the product is compatible with the product isomorphism: the hom component composed with Prod.fst equals Limits.prod.fst.

Русский

Первая проекция произведения совместима с изоморфизмом произведения: композиция гомоморна с Prod.fst даёт Limits.prod.fst.

LaTeX

$$$$ (binaryProductIso X Y).hom \\circ Prod.fst = Limits.prod.fst $$$$

Lean4

@[elementwise (attr := simp)]
theorem binaryProductIso_hom_comp_fst (X Y : Type u) : (binaryProductIso X Y).hom ≫ _root_.Prod.fst = Limits.prod.fst :=
  limit.isoLimitCone_hom_π (binaryProductLimitCone X Y) ⟨WalkingPair.left⟩

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