Theorem Ordinal.lift_typein_top

Modification history

2024-10-22 17:45
Mathlib/SetTheory/Ordinal/Basic.lean
chore(SetTheory/Ordinal/Basic): golf `Ordinal.lift` lemmas (#17517) …
Added Ordinal.lift_typein_topView on Github →