source
@[inline]
def LE.ofOrd (α : Type u) [Ord α] :
LE α

Creates an `LE α` instance from an `Ord α` instance.

`OrientedOrd α` must be satisfied so that the resulting `LE α` instance faithfully represents the `Ord α` instance.

Equations

- LE.ofOrd α = { le := fun (a b : α) => (compare a b).isLE = true }

Instances For

source
@[inline]
def DecidableLE.ofOrd (α : Type u) [LE α] [Ord α] [Std.LawfulOrderOrd α] :
DecidableLE α

Creates an `DecidableLE α` instance using a well-behaved `Ord α` instance.

Equations

- DecidableLE.ofOrd α a b = match h : (compare a b).isLE with | true => isTrue ⋯ | false => isFalse ⋯

Instances For

source
@[inline]
def LT.ofOrd (α : Type u) [Ord α] :
LT α

Creates an `LT α` instance from an `Ord α` instance.

`OrientedOrd α` must be satisfied so that the resulting `LT α` instance faithfully represents the `Ord α` instance.

Equations

- LT.ofOrd α = { lt := fun (a b : α) => compare a b = Ordering.lt }

Instances For

source
theorem Std.isLE_compare {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] {a b : α} :
(compare a b).isLE = true ↔ a ≤ b
source
theorem Std.isGE_compare {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] {a b : α} :
(compare a b).isGE = true ↔ b ≤ a
source
theorem Std.compare_eq_lt {α : Type u} [Ord α] [LT α] [LE α] [LawfulOrderOrd α] [LawfulOrderLT α] {a b : α} :
compare a b = Ordering.lt ↔ a < b
source
theorem Std.compare_eq_gt {α : Type u} [Ord α] [LT α] [LE α] [LawfulOrderOrd α] [LawfulOrderLT α] {a b : α} :
compare a b = Ordering.gt ↔ b < a
source
theorem Std.compare_eq_eq {α : Type u} [Ord α] [BEq α] [LE α] [LawfulOrderOrd α] [LawfulOrderBEq α] {a b : α} :
compare a b = Ordering.eq ↔ (a == b) = true
source
@[inline]
def DecidableLT.ofOrd (α : Type u) [LE α] [LT α] [Ord α] [Std.LawfulOrderOrd α] [Std.LawfulOrderLT α] :
DecidableLT α

Creates a `DecidableLT α` instance using a well-behaved `Ord α` instance.

Equations

- DecidableLT.ofOrd α a b = if h : compare a b = Ordering.lt then isTrue ⋯ else isFalse ⋯

Instances For

source
@[inline]
def BEq.ofOrd (α : Type u) [Ord α] :
BEq α

Creates a `BEq α` instance from an `Ord α` instance.

Equations

- BEq.ofOrd α = { beq := fun (a b : α) => decide (compare a b = Ordering.eq) }

Instances For

source
instance Std.instLawfulOrderOrd_ofOrd (α : Type u) [Ord α] [OrientedOrd α] :
LawfulOrderOrd α

The `LE α` instance obtained from an `Ord α` instance is compatible with said `Ord α` instance if `compare` is oriented, i.e., `compare a b = .lt ↔ compare b a = .gt`.

source
instance Std.instLawfulOrderLT_ofOrd {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] :
LawfulOrderLT α

The `LT α` instance obtained from an `Ord α` instance is compatible with the `LE α` instance instance if `Ord α` is compatible with it.

source
instance Std.instLawfulOrderBEq_ofOrd {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] :
LawfulOrderBEq α

The `BEq α` instance obtained from an `Ord α` instance is compatible with the `LE α` instance instance if `Ord α` is compatible with it.