English
If α is a partial order and every pair is comparable via the relation CompRel (≤), then α can be equipped with a LinearOrder.
Русский
Если α — частичный порядок и для любых a,b выполняется CompRel(≤) a b, то на α можно ввести линейный порядок.
LaTeX
$$[PartialOrder α] \Rightarrow (∀ a b, CompRel(≤) a b) \Rightarrow LinearOrder α$$
Lean4
/-- A partial order where any two elements are comparable is a linear order. -/
def linearOrderOfComprel [PartialOrder α] [decLE : DecidableLE α] [decLT : DecidableLT α] [decEq : DecidableEq α]
(h : ∀ a b : α, CompRel (· ≤ ·) a b) : LinearOrder α
where
le_total := h
toDecidableLE := decLE
toDecidableEq := decEq
toDecidableLT := decLT
