Theorems · Definition · order theory

PredOrder.prelimitRecOn

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

Recursion principle on a well-founded partial PredOrder.

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

5 results in Mathlib

Foundations

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

Assumes

PartialOrderPredOrderWellFoundedGT