Theorems · Theorem · order theory

PredOrder.colimitRecOn_pred_of_not_isMin

∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : LinearOrder α] [inst_1 : PredOrder α]
  [inst_2 : WellFoundedGT α] (isMax : (a : α) → IsMax a → motive a)
  (pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isPredLimit : (a : α) → Order.IsPredLimit a → ((b : α) → a < b → motive b) → motive a) (hb : ¬IsMin b),
  PredOrder.colimitRecOn (Order.pred b) isMax pred isPredLimit =
    pred b hb (PredOrder.colimitRecOn b isMax pred isPredLimit)

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrderPredOrderWellFoundedGT