partialOrder

Mathlib.Data.DFinsupp.Lex

URI: https://scilib.ai/kg/mathlib#DFinsupp.Lex.partialOrder

Lean4

/-- The partial order on `DFinsupp`s obtained by the lexicographic ordering.
See `DFinsupp.Lex.linearOrder` for a proof that this partial order is in fact linear. -/
instance partialOrder [∀ i, PartialOrder (α i)] : PartialOrder (Lex (Π₀ i, α i))
    where
  lt := (· < ·)
  le x y := ⇑(ofLex x) = ⇑(ofLex y) ∨ x < y
  __ := PartialOrder.lift (fun x : Lex (Π₀ i, α i) ↦ toLex (⇑(ofLex x))) (DFunLike.coe_injective (F := DFinsupp α))

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

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

Разделы

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

Аффилиация

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