Theorems · Definition · order theory

Order.isSuccLimitRecOn

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

A value can be built by building it on minimal elements, successors, and successor limits.

Defined in

Mathlib.Order.SuccPred.Limit

Cited by

4 results in Mathlib

Foundations

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

Assumes

PartialOrderSuccOrder