Theorem Order.IsSuccPrelimit.isLUB_Iio

Modification history

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