min and max in linearly ordered groups. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[simp]
theorem
max_zero_sub_max_neg_zero_eq_self
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
(a : α) :
linear_order.max a 0 - linear_order.max (-a) 0 = a
@[simp]
theorem
max_one_div_max_inv_one_eq_self
{α : Type u_1}
[group α]
[linear_order α]
[covariant_class α α has_mul.mul has_le.le]
(a : α) :
linear_order.max a 1 / linear_order.max a⁻¹ 1 = a
theorem
max_zero_sub_eq_self
{α : Type u_1}
[add_group α]
[linear_order α]
[covariant_class α α has_add.add has_le.le]
(a : α) :
linear_order.max a 0 - linear_order.max (-a) 0 = a
Alias of max_zero_sub_max_neg_zero_eq_self.
theorem
min_neg_neg
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b : α) :
linear_order.min (-a) (-b) = -linear_order.max a b
theorem
min_inv_inv'
{α : Type u_1}
[linear_ordered_comm_group α]
(a b : α) :
linear_order.min a⁻¹ b⁻¹ = (linear_order.max a b)⁻¹
theorem
max_inv_inv'
{α : Type u_1}
[linear_ordered_comm_group α]
(a b : α) :
linear_order.max a⁻¹ b⁻¹ = (linear_order.min a b)⁻¹
theorem
max_neg_neg
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b : α) :
linear_order.max (-a) (-b) = -linear_order.min a b
theorem
min_div_div_right'
{α : Type u_1}
[linear_ordered_comm_group α]
(a b c : α) :
linear_order.min (a / c) (b / c) = linear_order.min a b / c
theorem
min_sub_sub_right
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b c : α) :
linear_order.min (a - c) (b - c) = linear_order.min a b - c
theorem
max_div_div_right'
{α : Type u_1}
[linear_ordered_comm_group α]
(a b c : α) :
linear_order.max (a / c) (b / c) = linear_order.max a b / c
theorem
max_sub_sub_right
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b c : α) :
linear_order.max (a - c) (b - c) = linear_order.max a b - c
theorem
min_div_div_left'
{α : Type u_1}
[linear_ordered_comm_group α]
(a b c : α) :
linear_order.min (a / b) (a / c) = a / linear_order.max b c
theorem
min_sub_sub_left
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b c : α) :
linear_order.min (a - b) (a - c) = a - linear_order.max b c
theorem
max_div_div_left'
{α : Type u_1}
[linear_ordered_comm_group α]
(a b c : α) :
linear_order.max (a / b) (a / c) = a / linear_order.min b c
theorem
max_sub_sub_left
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b c : α) :
linear_order.max (a - b) (a - c) = a - linear_order.min b c
theorem
max_sub_max_le_max
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b c d : α) :
linear_order.max a b - linear_order.max c d ≤ linear_order.max (a - c) (b - d)
theorem
abs_max_sub_max_le_max
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b c d : α) :
|linear_order.max a b - linear_order.max c d| ≤ linear_order.max |a - c| |b - d|
theorem
abs_min_sub_min_le_max
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b c d : α) :
|linear_order.min a b - linear_order.min c d| ≤ linear_order.max |a - c| |b - d|
theorem
abs_max_sub_max_le_abs
{α : Type u_1}
[linear_ordered_add_comm_group α]
(a b c : α) :
|linear_order.max a c - linear_order.max b c| ≤ |a - b|