instLinearOrder

Mathlib.Data.List.Lex

URI: https://scilib.ai/kg/mathlib#List.instLinearOrder

Lean4

instance [LinearOrder α] : LinearOrder (List α) :=
  have : ∀ {r} [IsStrictTotalOrder α r], IsStrictTotalOrder (List α) (Lex r) :=
    { isStrictWeakOrder_of_isOrderConnected with }
  linearOrderOfSTO
    (Lex (· < ·))
      --Note: this overrides an instance in core lean

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

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

Разделы

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

Аффилиация

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