Theorem Ordinal.isSuccLimit_add_iff_of_isSuccLimit

Modification history

2025-08-31 01:28
Mathlib/SetTheory/Ordinal/Arithmetic.lean
feat(SetTheory/Cardinal/Aleph): `IsStrongLimit (preBeth x)` (#26895)
Added Ordinal.isSuccLimit_add_iff_of_isSuccLimitView on Github →