Commit 2024-08-23 14:42 50c45c0d

View on Github →

feat(Order/SuccPred/Limit): mem_range_succ_or_isSuccLimit (#15905)

Estimated changes

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.mem_range_pred_or_isPredLimit

added theorem Order.mem_range_succ_or_isSuccLimit