binaryProductCone

Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

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

Lean4

/-- The binary fan whose point is `prod F G`. -/
@[simps!]
def binaryProductCone : BinaryFan F G :=
  BinaryFan.mk prod.fst prod.snd

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

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

Разделы

Аффилиация

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