Theorem Ordinal.boundedLimitRec_succ

Modification history

2025-07-11 17:39
Mathlib/SetTheory/Ordinal/Arithmetic.lean
refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit` (#26643) …
Modified Ordinal.boundedLimitRec_succView on Github →
2025-04-11 21:03
Mathlib/SetTheory/Ordinal/Arithmetic.lean
chore: fix yet more induction branch names (#23686) …
Modified Ordinal.boundedLimitRec_succView on Github →
2024-10-04 21:26
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat (Mathlib/SetTheory/Ordinal/Arithmetic): add bounded recursion on ordinals (#16663) …
Added Ordinal.boundedLimitRec_succView on Github →