mathlib.order

en · official · sha256:4c75211e27319e193d0cc52dd48d5805d358ca8d55b49c602fde26ca00d8d8aa

class LinearOrder (α : Type*) extends PartialOrder α, Min α, Max α, Ord α where /-- A linear order is total. -/ protected le_total (a b : α) : a ≤ b ∨ b ≤ a /-- In a linearly ordered type, we assume the order relations are all decidable. -/ toDecidableLE : DecidableLE α /-- In a linearly ordered type, we assume the order relations are all decidable. -/ toDecidableEq : DecidableEq α := @decidableEqOfDecidableLE _ _ toDecidableLE /-- In a linearly ordered type, we assume the order relations are all decidable. -/ toDecidableLT : DecidableLT α := @decidableLTOfDecidableLE _ _ toDecidableLE min := fun a b => if a ≤ b then a else b max := fun a b => if a ≤ b then b else a /-- The minimum function is equivalent to the one you get from `minOfLe`. -/ protected min_def : ∀ a b, min a b = if a ≤ b then a else b := by intros; rfl /-- The minimum function is equivalent to the one you get from `maxOfLe`. -/ protected max_def : ∀ a b, max a b = if a ≤ b then b else a := by intros; rfl compare a b := compareOfLessAndEq a b /-- Comparison via `compare` is equal to the canonical comparison given decidable `<` and `=`. -/ compare_eq_compareOfLessAndEq : ∀ a b, compare a b = compareOfLessAndEq a b := by compareOfLessAndEq_rfl

Referencing norms: Import_Rule_fe781d4b45f1c0e419bffbc13071c03144c7491b558ca2f2bfff627e57c43adc