Theorems · Theorem · order theory

SuccOrder.prelimitRecOn_succ_of_not_isMax

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

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderSuccOrderWellFoundedLT