Theorem Ordinal.type_lt_withTop

Modification history

2026-10-01 14:50
Mathlib/SetTheory/Ordinal/Basic.lean
feat(SetTheory/Ordinal): definition of addition and multiplication (#43588) …
Added Ordinal.type_lt_withTopView on Github →