Wedge

Mathlib.CategoryTheory.Limits.Shapes.End

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Wedge

Lean4

/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, a wedge for `F` is a type of cones (specifically
the type of multiforks for `multicospanIndexEnd F`):
the point of universal of these wedges shall be the end of `F`. -/
abbrev Wedge :=
  Multifork (multicospanIndexEnd F)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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