The basic order typeclasses are in the core lean library in init/algebra/order.lean .
Basic typeclasses.
partial_orderdecidable_linear_order(a total order)
Usage examples.
variable (P₁ : Type*)
variable [partial_order P₁]
variables a b : P₁
example : a = b ↔ a ≤ b ∧ b ≤ a := le_antisymm_iff
example : a ≤ b → a < b ∨ a = b := lt_or_eq_of_le
variable (P₂ : Type*)
variable [decidable_linear_order P₂]
variables (c d e : P₂)
example : c < d ∨ c ≥ d := lt_or_ge c d
example (h₁ : c ≤ e) (h₂ : d ≤ e) : max c d ≤ e := max_le h₁ h₂
example : min (min c d) e = min c (min d e) := min_assoc c d e
Related typeclasses.
preorder, linear_order (a “non-decidable” linear order so you can’t use max or min!), ordered_cancel_comm_monoid, ordered_semiring (the naturals!) and so on. Note also the well_founded inductive type in init/wf.lean in the core library.
Advertisements
