Theoremsmap_max, map_min, map_max, map_min, left_comm, right_comm, map_max, map_min, map_max, map_min, instAssociativeMax, instAssociativeMin, instCommutativeMax, instCommutativeMin, instLawfulOrderInf_mathlib, instLawfulOrderSup_mathlib, le_max_iff, le_max_of_le_left, le_max_of_le_right, le_min_iff, le_of_max_le_left, le_of_max_le_right, lt_max_iff, lt_max_of_lt_left, lt_max_of_lt_right, lt_min_iff, max_cases, max_choice, max_eq_iff, max_eq_left_iff, max_eq_right_iff, max_idem, max_le_iff, max_le_max, max_le_max_left, max_le_max_right, max_left_commutative, max_lt_iff, max_lt_max, max_lt_max_left_iff, max_lt_max_right_iff, max_min_distrib_left, max_min_distrib_right, min_cases, min_choice, min_eq_iff, min_eq_left_iff, min_eq_right_iff, min_idem, min_le_iff, min_le_max, min_le_min, min_le_min_left, min_le_min_right, min_le_of_left_le, min_le_of_right_le, min_left_commutative, min_lt_iff, min_lt_max, min_lt_min, min_lt_min_left_iff, min_lt_min_right_iff, min_lt_of_left_lt, min_lt_of_right_lt, min_max_distrib_left, min_max_distrib_right, min_right_comm | 67 |