linearOrder

Mathlib.Data.Sigma.Order

URI: https://scilib.ai/kg/mathlib#Sigma.Lex.linearOrder

Lean4

/-- The lexicographical linear order on a sigma type. -/
instance linearOrder [LinearOrder ι] [∀ i, LinearOrder (α i)] : LinearOrder (Σₗ i, α i) :=
  { Lex.partialOrder with
    le_total := total_of ((Lex (· < ·)) fun _ => (· ≤ ·)), toDecidableEq := Sigma.instDecidableEqSigma
    toDecidableLE := Lex.decidable _ _
    toDecidableLT := Lex.decidable _ _ }

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

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

Разделы

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

Аффилиация

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