Commit 2026-03-24 19:17 d838828d

View on Github →

chore(Order/MinMax): use to_dual (#36972) This PR uses to_dual on some declarations about max/min. This file, Order.MinMax, is mostly silly now because the max/min theorems are copies of the same sup/inf declarations, except specialized to linear orders.

Estimated changes

deleted theorem AntitoneOn.map_min
deleted theorem Max.left_comm
deleted theorem Max.right_comm
deleted theorem MonotoneOn.map_min
deleted theorem max_cases
deleted theorem max_choice
deleted theorem max_eq_iff
deleted theorem max_eq_left_iff
deleted theorem max_eq_right_iff
deleted theorem max_le_iff
deleted theorem max_lt_iff
deleted theorem max_lt_max_left_iff
deleted theorem max_lt_max_right_iff
deleted theorem min_le_iff
deleted theorem min_le_min
deleted theorem min_le_min_left
deleted theorem min_le_min_right
deleted theorem min_le_of_left_le
deleted theorem min_le_of_right_le
deleted theorem min_left_commutative
deleted theorem min_lt_iff
deleted theorem min_lt_min
deleted theorem min_lt_of_left_lt
deleted theorem min_lt_of_right_lt
deleted theorem min_max_distrib_left
deleted theorem min_max_distrib_right
modified theorem min_right_comm