Theorem Order.IsPredPrelimit.lt_iff_exists_lt

Modification history

2026-03-05 10:25

Mathlib/Order/SuccPred/Limit.lean

chore(Order/SuccPred/Limit): use `to_dual` on everything that was missing (#35639)

Deleted Order.IsPredPrelimit.lt_iff_exists_lt View on Github →

2024-09-23 19:41

Mathlib/Order/SuccPred/Limit.lean

feat(Order/SuccPred/Limit): `IsSuccPrelimit.le_iff_forall_le` (#17026)

Added Order.IsPredPrelimit.lt_iff_exists_lt View on Github →