binaryProductLimitCone

Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FunctorToTypes.binaryProductLimitCone

Lean4

/-- `prod F G` is a binary product for `F` and `G`. -/
def binaryProductLimitCone : Limits.LimitCone (pair F G) :=
  ⟨_, binaryProductLimit F G⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru