Theorem Ordinal.toType_noMax_of_succ_lt

Modification history

2025-12-08 05:19

Mathlib/SetTheory/Ordinal/Arithmetic.lean

refactor: `Ordinal.toType` → `Ordinal.ToType` (#32449) …

Modified Ordinal.toType_noMax_of_succ_lt View on Github →

2024-08-27 18:38

Mathlib/SetTheory/Ordinal/Arithmetic.lean

chore(SetTheory/Ordinal/*): `o.out.α` → `o.toType` (#16161) …

Added Ordinal.toType_noMax_of_succ_lt View on Github →