source
class Std.LawfulOrderOrd (α : Type u) [Ord α] [LE α] :
Prop

This typeclass states that the synthesized `Ord α` instance is compatible with the `LE α` instance. This means that according to `compare`, the following are equivalent:

- `a` is less than or equal to `b` according to `compare`.
- `b` is greater than or equal to `b` according to `compare`.
- `a ≤ b` holds.

`LawfulOrderOrd α` automatically entails that `Ord α` is oriented (see `OrientedOrd α`) and that `LE α` is total.

`Ord α` and `LE α` mutually determine each other in the presence of `LawfulOrderOrd α`.

- isLE_compare (a b : α) : (compare a b).isLE = true ↔ a ≤ b
- isGE_compare (a b : α) : (compare a b).isGE = true ↔ b ≤ a

Instances

source
theorem Std.LawfulOrderOrd.isLE_compare_eq_false {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] {a b : α} :
(compare a b).isLE = false ↔ ¬a ≤ b
source
theorem Std.LawfulOrderOrd.isGE_compare_eq_false {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] {a b : α} :
(compare a b).isGE = false ↔ ¬b ≤ a