binaryProductIso_hom_comp_snd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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