Theorems · Definition · order theory

PredOrder.colimitRecOn

{α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : PredOrder α] →
          [WellFoundedGT α] →
            ((a : α) → IsMax a → motive a) →
              ((a : α) → ¬IsMin a → motive a → motive (Order.pred a)) →
                ((a : α) → Order.IsPredLimit a → ((b : α) → a < b → motive b) → motive a) → motive b

Recursion principle on a well-founded partial PredOrder, separating out the case of a minimal element.

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

4 results in Mathlib

Foundations

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

Assumes

PartialOrderPredOrderWellFoundedGT