Commit 2023-01-03 18:46 21c7a6b1

View on Github →

feat: port Order.SuccPred.Limit (#1300)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsPredLimit.lt_pred

added theorem Order.IsPredLimit.lt_pred_iff

added theorem Order.IsPredLimit.pred_ne

added def Order.IsPredLimit

added theorem Order.IsSuccLimit.isMin_of_noMax

added theorem Order.IsSuccLimit.succ_lt

added theorem Order.IsSuccLimit.succ_lt_iff

added theorem Order.IsSuccLimit.succ_ne

added def Order.IsSuccLimit

added theorem Order.isPredLimitRecOn_limit

added theorem Order.isPredLimitRecOn_pred'

added theorem Order.isPredLimitRecOn_pred

added theorem Order.isPredLimit_iff

added theorem Order.isPredLimit_iff_lt_pred

added theorem Order.isPredLimit_iff_of_noMin

added theorem Order.isPredLimit_of_dense

added theorem Order.isPredLimit_of_pred_lt

added theorem Order.isPredLimit_of_pred_ne

added theorem Order.isPredLimit_toDual_iff

added theorem Order.isPredLimit_top

added theorem Order.isSuccLimitRecOn_limit

added theorem Order.isSuccLimitRecOn_succ'

added theorem Order.isSuccLimitRecOn_succ

added theorem Order.isSuccLimit_bot

added theorem Order.isSuccLimit_iff

added theorem Order.isSuccLimit_iff_of_noMax

added theorem Order.isSuccLimit_iff_succ_lt

added theorem Order.isSuccLimit_iff_succ_ne

added theorem Order.isSuccLimit_of_dense

added theorem Order.isSuccLimit_of_succ_lt

added theorem Order.isSuccLimit_of_succ_ne

added theorem Order.isSuccLimit_toDual_iff

added theorem Order.mem_range_pred_of_not_isPredLimit

added theorem Order.mem_range_succ_of_not_isSuccLimit

added theorem Order.not_isPredLimit

added theorem Order.not_isPredLimit_iff

added theorem Order.not_isPredLimit_iff_exists_covby

added theorem Order.not_isPredLimit_of_noMin

added theorem Order.not_isPredLimit_pred

added theorem Order.not_isPredLimit_pred_of_not_isMin

added theorem Order.not_isSuccLimit

added theorem Order.not_isSuccLimit_iff'

added theorem Order.not_isSuccLimit_iff

added theorem Order.not_isSuccLimit_iff_exists_covby

added theorem Order.not_isSuccLimit_of_noMax

added theorem Order.not_isSuccLimit_succ

added theorem Order.not_isSuccLimit_succ_of_not_isMax