inclusionOfLinearOrder

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

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

Lean4

/-- The inclusion functor `WalkingMultispan (.ofLinearOrder ι) ⥤ WalkingMultispan (.prod ι)`. -/
@[simps!]
def inclusionOfLinearOrder (ι : Type w) [LinearOrder ι] :
    WalkingMultispan (.ofLinearOrder ι) ⥤ WalkingMultispan (.prod ι) :=
  MultispanIndex.multispan
    { left j := .left j.1
      right i := .right i
      fst j := WalkingMultispan.Hom.fst (J := .prod ι) j.1
      snd j := WalkingMultispan.Hom.snd (J := .prod ι) j.1 }

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

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

Разделы

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

Аффилиация

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