Theorem Order.isLUB_Iio_iff_isSuccPrelimit

Modification history

2025-01-13 10:02
Mathlib/Order/SuccPred/Limit.lean
feat: `IsSuccPrelimit a → IsLUB (Iio a) a` (#20496) …
Added Order.isLUB_Iio_iff_isSuccPrelimitView on Github →