Theorem Order.IsSuccLimit.isLUB_Iio

Modification history

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