Commit 2026-02-22 13:15 7862cbdf

View on Github →

chore(Order/SuccPred/Archimedean): use to_dual (#34882)

Estimated changes

Modified Mathlib/Order/MinMax.lean

deleted theorem Antitone.map_min

deleted theorem Monotone.map_min

Modified Mathlib/Order/SuccPred/Archimedean.lean

deleted theorem BddBelow.exists_isLeast_of_nonempty

deleted theorem LE.le.exists_pred_iterate

deleted theorem Pred.rec

deleted theorem Pred.rec_iff

deleted theorem Pred.rec_linear

deleted theorem Pred.rec_top

added theorem StrictAnti.not_bddAbove_range_of_isSuccArchimedean

deleted theorem StrictAnti.not_bddBelow_range_of_isPredArchimedean

deleted theorem StrictAnti.not_bddBelow_range_of_isSuccArchimedean

deleted theorem StrictMono.not_bddBelow_range_of_isPredArchimedean

deleted theorem exists_pred_iterate_iff_le

deleted theorem exists_pred_iterate_or

deleted theorem le_total_of_directed

deleted theorem lt_or_le_of_directed

deleted theorem pred_max

deleted theorem pred_min

deleted theorem succ_max

deleted theorem succ_min

Modified Mathlib/Order/SuccPred/Basic.lean

deleted theorem Order.pred_mono

added theorem Order.succ_max

added theorem Order.succ_min