linearOrder

Mathlib.Data.Finsupp.Lex

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

Lean4

/-- The linear order on `Finsupp`s obtained by the lexicographic ordering. -/
instance linearOrder [LinearOrder N] : LinearOrder (Lex (α →₀ N))
    where
  lt := (· < ·)
  le := (· ≤ ·)
  __ := LinearOrder.lift' (toLex ∘ toDFinsupp ∘ ofLex) finsuppEquivDFinsupp.injective

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

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

Разделы

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

Аффилиация

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