Theorems · Definition · logic and foundations

Ordinal.limitRecOn

{motive : Ordinal.{u_5} → Sort u_4} →
  (o : Ordinal.{u_5}) →
    motive 0 →
      ((o : Ordinal.{u_5}) → motive o → motive (o + 1)) →
        ((o : Ordinal.{u_5}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_5}) → o' < o → motive o') → motive o) → motive o

Limit induction on ordinals: if one can prove a property by induction at successor ordinals and at limit ordinals, then it holds for all ordinals. Note that this is just a special (though sometimes convenient) case of the more general well-founded recursion WellFoundedLT.fix.

Defined in

Mathlib.SetTheory.Ordinal.Arithmetic

Cited by

20 results in Mathlib

Foundations

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