linearOrder — Mathlib

English

A simple partial order with decidable equality yields a total (linear) order.

Русский

Простой частичный порядок с разрешаемостью равенств даёт полный (линейный) порядок.

LaTeX

$$$\text{IsSimpleOrder}.\text{linearOrder} : LinearOrder α$$$

Lean4

/-- A simple partial ordered `BoundedOrder` induces a linear order.
This is not an instance to prevent loops. -/
protected def linearOrder [DecidableEq α] : LinearOrder α :=
  {
    (inferInstance :
      PartialOrder
        α) with
    le_total := fun a b => by
      rcases eq_bot_or_eq_top a with (rfl | rfl) <;>
        simp
          -- Note from https://github.com/leanprover-community/mathlib4/issues/23976: do we want this inlined or should this be a separate definition?

    toDecidableLE := fun a b =>
      if ha : a = ⊥ then isTrue (ha.le.trans bot_le)
      else
        if hb : b = ⊤ then isTrue (le_top.trans hb.ge)
        else isFalse fun H => hb (top_unique (le_trans (top_le_iff.mpr (Or.resolve_left (eq_bot_or_eq_top a) ha)) H))
    toDecidableEq := ‹_› }

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