min and max in linearly ordered groups.

ink

@[simp]

theorem max_zero_sub_max_neg_zero_eq_self {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) : max a 0 - max (-a) 0 = a

ink

@[simp]

theorem max_one_div_max_inv_one_eq_self {α : Type u_1} [inst : Group α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] (a : α) : max a 1 / max a⁻¹ 1 = a

ink

theorem max_zero_sub_eq_self {α : Type u_1} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) : max a 0 - max (-a) 0 = a

Alias of max_zero_sub_max_neg_zero_eq_self.

ink

theorem min_neg_neg {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) : min (-a) (-b) = -max a b

ink

theorem min_inv_inv' {α : Type u_1} [inst : LinearOrderedCommGroup α] (a : α) (b : α) : min a⁻¹ b⁻¹ = (max a b)⁻¹

ink

theorem max_neg_neg {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) : max (-a) (-b) = -min a b

ink

theorem max_inv_inv' {α : Type u_1} [inst : LinearOrderedCommGroup α] (a : α) (b : α) : max a⁻¹ b⁻¹ = (min a b)⁻¹

ink

theorem min_sub_sub_right {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : min (a - c) (b - c) = min a b - c

ink

theorem min_div_div_right' {α : Type u_1} [inst : LinearOrderedCommGroup α] (a : α) (b : α) (c : α) : min (a / c) (b / c) = min a b / c

ink

theorem max_sub_sub_right {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : max (a - c) (b - c) = max a b - c

ink

theorem max_div_div_right' {α : Type u_1} [inst : LinearOrderedCommGroup α] (a : α) (b : α) (c : α) : max (a / c) (b / c) = max a b / c

ink

theorem min_sub_sub_left {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : min (a - b) (a - c) = a - max b c

ink

theorem min_div_div_left' {α : Type u_1} [inst : LinearOrderedCommGroup α] (a : α) (b : α) (c : α) : min (a / b) (a / c) = a / max b c

ink

theorem max_sub_sub_left {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : max (a - b) (a - c) = a - min b c

ink

theorem max_div_div_left' {α : Type u_1} [inst : LinearOrderedCommGroup α] (a : α) (b : α) (c : α) : max (a / b) (a / c) = a / min b c

ink

theorem max_sub_max_le_max {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) (d : α) : max a b - max c d ≤ max (a - c) (b - d)

ink

theorem abs_max_sub_max_le_max {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) (d : α) : abs (max a b - max c d) ≤ max (abs (a - c)) (abs (b - d))

ink

theorem abs_min_sub_min_le_max {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) (d : α) : abs (min a b - min c d) ≤ max (abs (a - c)) (abs (b - d))

ink

theorem abs_max_sub_max_le_abs {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (c : α) : abs (max a c - max b c) ≤ abs (a - b)