Theorem Order.IsSuccLimit.nonempty_Iio

Modification history

2025-08-26 10:33
Mathlib/Order/SuccPred/Limit.lean
feat: `IsSuccLimit a → (Iio a).Nonempty` (#28946) …
Added Order.IsSuccLimit.nonempty_IioView on Github →