Theorem Ordinal.isLimit_omega0

Modification history

2024-12-05 05:55
Mathlib/SetTheory/Ordinal/Arithmetic.lean
refactor(SetTheory/Ordinal/Arithmetic): redefine `IsLimit` to `IsSuccLimit` (#19054) …
Modified Ordinal.isLimit_omega0View on Github →
2024-10-17 03:53
Mathlib/SetTheory/Ordinal/Arithmetic.lean
chore(SetTheory/Ordinal/Arithmetic): `omega0_isLimit` → `isLimit_omega0` (#17744) …
Added Ordinal.isLimit_omega0View on Github →