binaryProductLimitCone_cone_π_app_right

English

In the binary product limit cone, the right projection equals the morphism corresponding to snd.

Русский

В лимитном конусе двоичного произведения правое проецирование равно морфизму, соответствующему snd.

LaTeX

$$$ (binaryProductLimitCone G H).cone.\pi.app \langle WalkingPair.right \rangle = ofHom (AddMonoidHom.snd G H) $$$

Lean4

@[simp]
theorem binaryProductLimitCone_cone_π_app_right (G H : AddCommGrpCat.{u}) :
    (binaryProductLimitCone G H).cone.π.app ⟨WalkingPair.right⟩ = ofHom (AddMonoidHom.snd G H) :=
  rfl

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