ofLinearOrder

Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

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

Lean4

/-- The multicofork for `I : MultispanIndex (.prod ι) C` deduced from
a multicofork for `I.toLinearOrder` when `ι` is linearly ordered
and `I` is symmetric. -/
def ofLinearOrder (c : Multicofork I.toLinearOrder) (h : I.SymmStruct) : Multicofork I :=
  Multicofork.ofπ _ c.pt c.π
    (by
      rintro ⟨x, y⟩
      obtain hxy | rfl | hxy := lt_trichotomy x y
      · exact c.condition ⟨⟨x, y⟩, hxy⟩
      · simp [h.fst_eq_snd]
      · have := c.condition ⟨⟨y, x⟩, hxy⟩
        dsimp at this ⊢
        rw [← h.iso_hom_fst_assoc, ← h.iso_hom_snd_assoc, this])

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

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

Разделы

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

Аффилиация

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