binaryProductLimitCone_cone_π_app_left

English

The left projection in the constructed binary product limit cone equals the object morphism to M given by fst.

Русский

Левая проекция в ограничении произведения равна отображению fst на M.

LaTeX

$$$(binaryProductLimitCone M N).cone.\pi.app\langle WalkingPair.left \rangle = \mathrm{ofHom}(\mathrm{LinearMap.fst}\;R\;M\;N)$$$

Lean4

@[simp]
theorem binaryProductLimitCone_cone_π_app_left (M N : ModuleCat.{v} R) :
    (binaryProductLimitCone M N).cone.π.app ⟨WalkingPair.left⟩ = ofHom (LinearMap.fst R M N) :=
  rfl

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