Theorem Ordinal.type_uLift

Modification history

2026-02-24 13:32
Mathlib/SetTheory/Ordinal/Basic.lean
feat: more lemmas on `Ordinal.type` (#35519) …
Deleted Ordinal.type_uLiftView on Github →
2023-02-13 06:43
Mathlib/SetTheory/Ordinal/Basic.lean
feat: port SetTheory.Ordinal.Basic (#2217) …
Added Ordinal.type_uLiftView on Github →