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
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : min a b = if a ≤ b then a else b
• max_def (a b : α) : max 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 = { toLinearOrder := inst✝¹, toIsWellOrder := inst✝ }