Commit 2025-12-26 22:32 0ce4e625

View on Github →

chore: use to_dual on IsSuccPrelimit / IsSuccLimit (#33151)

Estimated changes

Modified Mathlib/Order/Cover.lean

Modified Mathlib/Order/SuccPred/Basic.lean

Modified Mathlib/Order/SuccPred/Limit.lean

deleted theorem Order.IsPredLimit.lt_pred

deleted theorem Order.IsPredLimit.lt_pred_iff

deleted theorem Order.IsPredLimit.lt_top

deleted theorem Order.IsPredLimit.ne_top

deleted theorem Order.IsPredLimit.pred_le_iff

deleted theorem Order.IsPredLimit.pred_ne

deleted def Order.IsPredLimit

deleted theorem Order.IsPredPrelimit.isPredLimit

deleted theorem Order.IsPredPrelimit.isPredLimit_of_not_isMax

deleted theorem Order.IsPredPrelimit.lt_pred

deleted theorem Order.IsPredPrelimit.lt_pred_iff

deleted theorem Order.IsPredPrelimit.of_dense

deleted theorem Order.IsPredPrelimit.pred_le_iff

deleted theorem Order.IsPredPrelimit.pred_ne

deleted def Order.IsPredPrelimit

deleted theorem Order.isPredLimitRecOn_of_isMax

deleted theorem Order.isPredLimitRecOn_of_isPredLimit

deleted theorem Order.isPredLimitRecOn_pred

deleted theorem Order.isPredLimitRecOn_pred_of_not_isMin

deleted theorem Order.isPredLimit_iff

deleted theorem Order.isPredPrelimitRecOn_of_isPredPrelimit

deleted theorem Order.isPredPrelimitRecOn_pred

deleted theorem Order.isPredPrelimitRecOn_pred_of_not_isMin

deleted theorem Order.isPredPrelimit_iff_isPredLimit

deleted theorem Order.isPredPrelimit_iff_isPredLimit_of_not_isMax

deleted theorem Order.isPredPrelimit_iff_lt_pred

deleted theorem Order.isPredPrelimit_iff_pred_ne

deleted theorem Order.isPredPrelimit_of_pred_lt

deleted theorem Order.isPredPrelimit_of_pred_ne

deleted theorem Order.isPredPrelimit_toDual_iff

deleted theorem Order.isPredPrelimit_top

deleted theorem Order.mem_range_pred_of_not_isPredPrelimit

deleted theorem Order.mem_range_pred_or_isPredPrelimit

deleted theorem Order.not_isPredLimit_iff

deleted theorem Order.not_isPredLimit_pred

deleted theorem Order.not_isPredLimit_pred_of_not_isMin

deleted theorem Order.not_isPredLimit_top

deleted theorem Order.not_isPredPrelimit_iff'

deleted theorem Order.not_isPredPrelimit_iff

deleted theorem Order.not_isPredPrelimit_iff_exists_covBy

deleted theorem Order.not_isPredPrelimit_pred

deleted theorem Order.not_isPredPrelimit_pred_of_not_isMin

deleted theorem PredOrder.limitRecOn_isMax

deleted theorem PredOrder.limitRecOn_of_isPredLimit

deleted theorem PredOrder.limitRecOn_pred

deleted theorem PredOrder.limitRecOn_pred_of_not_isMin

deleted theorem PredOrder.prelimitRecOn_of_isPredPrelimit

deleted theorem PredOrder.prelimitRecOn_pred

deleted theorem PredOrder.prelimitRecOn_pred_of_not_isMin

Modified Mathlib/Tactic/Translate/ToDual.lean