Theorem Cardinal.isLimit_ord

Modification history

2025-07-11 17:39

Mathlib/SetTheory/Ordinal/Arithmetic.lean

refactor(SetTheory/Ordinal/Arithmetic): `Ordinal.IsLimit` → `Order.IsSuccLimit` (#26643) …

Deleted Cardinal.isLimit_ord View on Github →

2024-10-17 03:53

Mathlib/SetTheory/Ordinal/Arithmetic.lean

chore(SetTheory/Ordinal/Arithmetic): `omega0_isLimit` → `isLimit_omega0` (#17744) …

Added Cardinal.isLimit_ord View on Github →