Commit 2022-11-26 03:55 315d3a6d

View on Github →

feat: port order.minmax (#728) Port of order.minmax Based on 71ca477041bcd6d7c745fe555dc49735c12944b7

Estimated changes

added theorem Antitone.map_max
added theorem Antitone.map_min
added theorem AntitoneOn.map_max
added theorem AntitoneOn.map_min
added theorem Max.left_comm
added theorem Max.right_comm
added theorem Monotone.map_max
added theorem Monotone.map_min
added theorem MonotoneOn.map_max
added theorem MonotoneOn.map_min
added theorem le_max_iff
added theorem le_max_of_le_left
added theorem le_max_of_le_right
added theorem le_min_iff
added theorem le_of_max_le_left
added theorem le_of_max_le_right
added theorem lt_max_iff
added theorem lt_max_of_lt_left
added theorem lt_max_of_lt_right
added theorem lt_min_iff
added theorem max_associative
added theorem max_cases
added theorem max_choice
added theorem max_commutative
added theorem max_eq_iff
added theorem max_eq_left_iff
added theorem max_eq_right_iff
added theorem max_le_iff
added theorem max_le_max
added theorem max_left_commutative
added theorem max_lt_iff
added theorem max_lt_max
added theorem max_lt_max_left_iff
added theorem max_lt_max_right_iff
added theorem max_min_distrib_left
added theorem max_min_distrib_right
added theorem min_associative
added theorem min_cases
added theorem min_choice
added theorem min_commutative
added theorem min_eq_iff
added theorem min_eq_left_iff
added theorem min_eq_right_iff
added theorem min_le_iff
added theorem min_le_max
added theorem min_le_min
added theorem min_le_of_left_le
added theorem min_le_of_right_le
added theorem min_left_commutative
added theorem min_lt_iff
added theorem min_lt_max
added theorem min_lt_min
added theorem min_lt_min_left_iff
added theorem min_lt_min_right_iff
added theorem min_lt_of_left_lt
added theorem min_lt_of_right_lt
added theorem min_max_distrib_left
added theorem min_max_distrib_right
added theorem min_right_comm