Documentation

Mathlib.Algebra.Order.Group.MinMax

min and max in linearly ordered groups. #

@[simp]
theorem max_zero_sub_max_neg_zero_eq_self {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
max a 0 - max (-a) 0 = a
@[simp]
theorem max_one_div_max_inv_one_eq_self {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
max a 1 / max a⁻¹ 1 = a
theorem max_zero_sub_eq_self {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
max a 0 - max (-a) 0 = a

Alias of max_zero_sub_max_neg_zero_eq_self.

theorem max_neg_zero {α : Type u_1} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 x2] (a : α) :
max (-a) 0 = -a + max a 0
theorem max_inv_one {α : Type u_1} [Group α] [LinearOrder α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 x2] (a : α) :
max a⁻¹ 1 = a⁻¹ * max a 1
theorem min_neg_neg {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) :
min (-a) (-b) = -max a b
theorem min_inv_inv' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) :
theorem max_neg_neg {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) :
max (-a) (-b) = -min a b
theorem max_inv_inv' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) :
theorem min_sub_sub_right {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) :
min (a - c) (b - c) = min a b - c
theorem min_div_div_right' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) (c : α) :
min (a / c) (b / c) = min a b / c
theorem max_sub_sub_right {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) :
max (a - c) (b - c) = max a b - c
theorem max_div_div_right' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) (c : α) :
max (a / c) (b / c) = max a b / c
theorem min_sub_sub_left {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) :
min (a - b) (a - c) = a - max b c
theorem min_div_div_left' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) (c : α) :
min (a / b) (a / c) = a / max b c
theorem max_sub_sub_left {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) :
max (a - b) (a - c) = a - min b c
theorem max_div_div_left' {α : Type u_1} [LinearOrderedCommGroup α] (a : α) (b : α) (c : α) :
max (a / b) (a / c) = a / min b c
theorem max_sub_max_le_max {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) (d : α) :
max a b - max c d max (a - c) (b - d)
theorem abs_max_sub_max_le_max {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) (d : α) :
|max a b - max c d| max |a - c| |b - d|
theorem abs_min_sub_min_le_max {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) (d : α) :
|min a b - min c d| max |a - c| |b - d|
theorem abs_max_sub_max_le_abs {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) :
|max a c - max b c| |a - b|