Theorems · Theorem · order theory

Order.isPredPrelimitRecOn_pred_of_not_isMin

∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α]
  (pred : (a : α) → ¬IsMin a → motive (Order.pred a)) (isPredPrelimit : (a : α) → Order.IsPredPrelimit a → motive a)
  (hb : ¬IsMin b), Order.isPredPrelimitRecOn (Order.pred b) pred isPredPrelimit = pred b hb

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

2 results in Mathlib

Foundations

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

Assumes

LinearOrderPredOrder