Theorems · Theorem · logic and foundations

Ordinal.limitRecOn_limit

∀ {motive : Ordinal.{u_4} → Sort u_5} (o : Ordinal.{u_4}) (H₁ : motive 0)
  (H₂ : (o : Ordinal.{u_4}) → motive o → motive (o + 1))
  (H₃ : (o : Ordinal.{u_4}) → Order.IsSuccLimit o → ((o' : Ordinal.{u_4}) → o' < o → motive o') → motive o)
  (h : Order.IsSuccLimit o), Ordinal.limitRecOn o H₁ H₂ H₃ = H₃ o h fun x _h => Ordinal.limitRecOn x H₁ H₂ H₃

Defined in

Mathlib.SetTheory.Ordinal.Arithmetic

Cited by

2 results in Mathlib

Foundations

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