Theorem Ordinal.isSuccPrelimit_type_lt

Modification history

2026-02-24 13:32
Mathlib/SetTheory/Ordinal/Basic.lean
feat: more lemmas on `Ordinal.type` (#35519) …
Added Ordinal.isSuccPrelimit_type_ltView on Github →