Theorem Ordinal.liftOnWellOrder_type

Modification history

2024-12-12 20:12
Mathlib/SetTheory/Ordinal/Basic.lean
feat(SetTheory/Ordinal/Basic): recursion on well-orders (#19678) …
Added Ordinal.liftOnWellOrder_typeView on Github →