toLinearOrder

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

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

Lean4

/-- The multispan index for `MultispanShape.ofLinearOrder ι` deduced from
a multispan index for `MultispanShape.prod ι` when `ι` is linearly ordered. -/
@[simps]
def toLinearOrder : MultispanIndex (.ofLinearOrder ι) C
    where
  left j := I.left j.1
  right i := I.right i
  fst j := I.fst j.1
  snd j := I.snd j.1

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

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

Разделы

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

Аффилиация

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