@[instance_reducible, 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 }

@[instance_reducible, 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 ⋯

@[instance_reducible, 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 }

theorem Std.isLE_compare {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] {a b : α} : (compare a b).isLE = true ↔ a ≤ b

theorem Std.isGE_compare {α : Type u} [Ord α] [LE α] [LawfulOrderOrd α] {a b : α} : (compare a b).isGE = true ↔ b ≤ a

theorem Std.compare_eq_lt {α : Type u} [Ord α] [LT α] [LE α] [LawfulOrderOrd α] [LawfulOrderLT α] {a b : α} : compare a b = Ordering.lt ↔ a < b

theorem Std.compare_eq_gt {α : Type u} [Ord α] [LT α] [LE α] [LawfulOrderOrd α] [LawfulOrderLT α] {a b : α} : compare a b = Ordering.gt ↔ b < a

theorem Std.compare_eq_eq {α : Type u} [Ord α] [BEq α] [LE α] [LawfulOrderOrd α] [LawfulOrderBEq α] {a b : α} : compare a b = Ordering.eq ↔ (a == b) = true

theorem Std.compare_ne_eq {α : Type u} [Ord α] [BEq α] [LE α] [LawfulOrderOrd α] [LawfulOrderBEq α] {a b : α} : compare a b ≠ Ordering.eq ↔ ¬(a == b) = true

theorem Std.compare_ne_eq_iff_ne {α : Type u} [Ord α] [LawfulEqOrd α] {a b : α} : compare a b ≠ Ordering.eq ↔ a ≠ b

@[instance_reducible, 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 ⋯

@[instance_reducible, 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) }

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.

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.

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.