Theorems · Theorem · logic and foundations

Ordinal.limitRecOn_zero

∀ {motive : Ordinal.{u_4} → Sort u_5} (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),
  Ordinal.limitRecOn 0 H₁ 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