linearOrderOfCompares — Mathlib

English

If α is a preorder and cmp: α → α → Ordering is given with the property that for all a,b, (cmp a b).Compares a b, then there is a LinearOrder on α constructed from cmp. In other words, cmp defines a total, transitive order on α.

Русский

Пусть α задаёт порядок пределов (preorder) и cmp: α → α → Ordering — сравнение, удовлетворяющее условию, что для всех a,b выполняется (cmp a b).Compares a b. Тогда на α можно естественным образом ввести линейный порядок, задаваемый cmp.

LaTeX

$$$\exists \leq, < \text{ на } \alpha \text{ такие, что } a \le b \iff (cmp\,a\,b) \in \{\mathrm{Ordering.lt}, \mathrm{Ordering.eq}\},\; a < b \iff (cmp\,a\,b) = \mathrm{Ordering.lt}$$$

Lean4

/-- Generate a linear order structure from a preorder and `cmp` function. -/
def linearOrderOfCompares [Preorder α] (cmp : α → α → Ordering) (h : ∀ a b, (cmp a b).Compares a b) : LinearOrder α :=
  let H : DecidableLE α := fun a b => decidable_of_iff _ (h a b).ne_gt
  { inferInstanceAs (Preorder α) with le_antisymm := fun a b => (h a b).le_antisymm,
    le_total := fun a b => (h a b).le_total, toMin := minOfLe, toMax := maxOfLe, toDecidableLE := H,
    toDecidableLT := fun a b => decidable_of_iff _ (h a b).eq_lt,
    toDecidableEq := fun a b => decidable_of_iff _ (h a b).eq_eq }

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