Commit 2025-01-13 10:02 2c53e450

View on Github →

feat: IsSuccPrelimit a → IsLUB (Iio a) a (#20496) This is somewhat more general than the statement involving sSup.

Estimated changes

Modified Mathlib/Order/SuccPred/CompleteLinearOrder.lean

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsPredLimit.isGLB_Ioi

added theorem Order.IsPredPrelimit.isGLB_Ioi

added theorem Order.IsSuccLimit.isLUB_Iio

added theorem Order.IsSuccPrelimit.isLUB_Iio

added theorem Order.isGLB_Ioi_iff_isPredPrelimit

added theorem Order.isLUB_Iio_iff_isSuccPrelimit