binaryProductLimitCone_cone_π_app_left

English

In the binary product limit cone, the left projection equals the morphism corresponding to fst.

Русский

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

LaTeX

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

Lean4

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

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