class LtWellOrder (α : Type u_1) extends LinearOrder α, IsWellOrder α fun (x1 x2 : α) => x1 < x2 : Type u_1

• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2
• decidableEq : DecidableEq α
• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2
• min_def : ∀ (a b : α), a ⊓ b = if a ≤ b then a else b
• max_def : ∀ (a b : α), a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b = compareOfLessAndEq a b
• trichotomous : ∀ (a b : α), a < b ∨ a = b ∨ b < a
• trans : ∀ (a b c : α), a < b → b < c → a < c
• wf : WellFounded fun (x1 x2 : α) => x1 < x2

instance instLtWellOrderOfIsWellOrderLt {α : Type u_1} [LinearOrder α] [IsWellOrder α fun (x1 x2 : α) => x1 < x2] : LtWellOrder α

Equations

• instLtWellOrderOfIsWellOrderLt = LtWellOrder.mk