English
A lattice with a total order is a linear order; i.e., given a lattice α with decidable relations and a total ≤, one obtains a LinearOrder structure on α where the standard sup/inf are given by maxDefault/minDefault.
Русский
Ладица с полностью упорядоченной связью – линейный порядок: если заданы все отношения и порядок тотален, то над α образуется линейный порядок, причем максимум и минимум соответствуют maxDefault и minDefault.
LaTeX
$$$ ( ext{IsTotal } α (≤)) \Rightarrow ( ext{LinearOrder } α ) $$$
Lean4
/-- A lattice with total order is a linear order.
See note [reducible non-instances]. -/
abbrev toLinearOrder (α : Type u) [Lattice α] [DecidableEq α] [DecidableLE α] [DecidableLT α] [IsTotal α (· ≤ ·)] :
LinearOrder α where
toDecidableLE := ‹_›
toDecidableEq := ‹_›
toDecidableLT := ‹_›
le_total := total_of (· ≤ ·)
max_def := by exact congr_fun₂ sup_eq_maxDefault
min_def := by exact congr_fun₂ inf_eq_minDefault
