Theorem Ordinal.isLimit_iff

Modification history

2024-12-05 05:55

Mathlib/SetTheory/Ordinal/Arithmetic.lean

refactor(SetTheory/Ordinal/Arithmetic): redefine `IsLimit` to `IsSuccLimit` (#19054) …

Added Ordinal.isLimit_iff View on Github →