Theorems · Theorem · order theory

Order.isSuccPrelimitRecOn_succ

∀ {α : Type u_1} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : SuccOrder α]
  (succ : (a : α) → ¬IsMax a → motive (Order.succ a)) (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → motive a)
  [inst_2 : NoMaxOrder α] (b : α), Order.isSuccPrelimitRecOn (Order.succ b) succ isSuccPrelimit = succ b ⋯

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

1 results in Mathlib

Foundations

Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderSuccOrderNoMaxOrder