Def Ordinal.liftOnWellOrder

Modification history

2024-12-12 20:12

Mathlib/SetTheory/Ordinal/Basic.lean

feat(SetTheory/Ordinal/Basic): recursion on well-orders (#19678) …

Added Ordinal.liftOnWellOrder View on Github →