Theorem Ordinal.isLimit_of_not_succ_of_ne_zero

Modification history

2024-10-25 20:32

Mathlib/SetTheory/Ordinal/Arithmetic.lean

feat(SetTheory/Ordinal/Topology): define Ordinal.IsClosed and Ordinal.IsAcc (#16710) …

Added Ordinal.isLimit_of_not_succ_of_ne_zero View on Github →