Def Ordinal.boundedLimitRecOn

Modification history

2024-10-04 21:26

Mathlib/SetTheory/Ordinal/Arithmetic.lean

feat (Mathlib/SetTheory/Ordinal/Arithmetic): add bounded recursion on ordinals (#16663) …

Added Ordinal.boundedLimitRecOn View on Github →