Theorems · Definition · order theory

SuccOrder.limitRecOn

{α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : SuccOrder α] →
          [WellFoundedLT α] →
            ((a : α) → IsMin a → motive a) →
              ((a : α) → ¬IsMax a → motive a → motive (Order.succ a)) →
                ((a : α) → Order.IsSuccLimit a → ((b : α) → b < a → motive b) → motive a) → motive b

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

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

14 results in Mathlib

Foundations

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

Assumes

PartialOrderSuccOrderWellFoundedLT