The basic order typeclasses are in the core lean library in `init/algebra/order.lean`

.

## Basic typeclasses.

`partial_order`

`decidable_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