abs_min_sub_min_le_max
theorem abs_min_sub_min_le_max :
∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a b c d : α), |min a b - min c d| ≤ max |a - c| |b - d| := by
sorry
This theorem states that for any four values of a linear ordered additive commutative group type, the absolute value of the difference between the minimum of the first two values and the minimum of the last two values is always less than or equal to the maximum of the absolute values of the differences between the first and third values and the second and fourth values. In mathematical terms, for any elements $a$, $b$, $c$, $d$ in a linear ordered additive commutative group, $| \min(a, b) - \min(c, d) | \leq \max(|a - c|, |b - d|)$.
More concisely: For any elements $a, b, c, d$ in a linear ordered additive commutative group, the absolute difference between the minimum of $a$ and $b$ and the minimum of $c$ and $d$ is less than or equal to the maximum of the absolute differences between $a$ and $c$, and $b$ and $d$. In symbols, $| \min(a, b) - \min(c, d) | \leq \max(|a - c|, |b - d|)$.
|
max_zero_sub_max_neg_zero_eq_self
theorem max_zero_sub_max_neg_zero_eq_self :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α), max a 0 - max (-a) 0 = a
This theorem, `max_zero_sub_max_neg_zero_eq_self`, states that for any type `α` that is an additive group and has a linear order and a covariant class, the maximum of a given element `a` and zero, subtracted by the maximum of the negative of `a` and zero, equals `a` itself. In mathematical notations, this can be represented as: max(a, 0) - max(-a, 0) = a. This theorem essentially provides a relationship between an element and its additive inverse in the context of maximum and subtraction operations.
More concisely: For any additive group with a linear order and a covariant class, max(a, 0) - max(-a, 0) = a.
|
max_zero_sub_eq_self
theorem max_zero_sub_eq_self :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α), max a 0 - max (-a) 0 = a
This theorem, `max_zero_sub_eq_self`, is an alias of `max_zero_sub_max_neg_zero_eq_self`. It states that for any arbitrary variable `a` of some type `α`, where `α` is an additive group and linear order with the property that addition (`x + x_1`) implies an ordering relation (`x ≤ x_1`), the difference of the maximum of `a` and zero and the maximum of negative `a` and zero is equal to `a` itself. This theorem applies to any type that has these algebraic structures and properties.
More concisely: For any additive group and linear order type `α` where `x + x_1` implies `x ≤ x_1`, the maximum of `a` and `-a` equals `2 * max(abs(a), 0)`.
|
abs_max_sub_max_le_max
theorem abs_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| := by
sorry
This theorem establishes a relationship among the maximum values and absolute differences of four elements, `a`, `b`, `c`, and `d`, in any linear ordered additive commutative group, which is a mathematical structure that combines the properties of being a group and a linear order. The theorem states that the absolute value of the difference between the maximum of `a` and `b` and the maximum of `c` and `d` is always less than or equal to the maximum of the absolute differences of `a` and `c` and `b` and `d`. This property provides an upper bound for the absolute difference between two maxima.
More concisely: In any linear ordered additive commutative group, |max(a, b) - max(c, d)| ≤ max(|a - c|, |b - d|).
|
min_neg_neg
theorem min_neg_neg : ∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a b : α), min (-a) (-b) = -max a b := by
sorry
This theorem, `min_neg_neg`, states that for all types `α` that form a linearly ordered additive commutative group, for any two elements `a` and `b` of this type, the minimum of the negations of `a` and `b` is equal to the negation of the maximum of `a` and `b`. In mathematical terms, it says that $\min(-a, -b) = -\max(a, b)$ for all $a, b$ in a given linearly ordered additive commutative group.
More concisely: For all linearly ordered additive commutative groups (α, +, <) and all a, b ∈ α, we have -(min(a, b)) = max(a, b).
|
max_neg_neg
theorem max_neg_neg : ∀ {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a b : α), max (-a) (-b) = -min a b := by
sorry
This theorem, named `max_neg_neg`, states that for any type `α` that is a linearly ordered additive commutative group, the maximum of the negations of two elements `a` and `b` is equal to the negation of the minimum of `a` and `b`. In other words, it's saying that the maximum of `-a` and `-b` is the same as `-min(a, b)`. This theorem is applicable to any set where the elements can be ordered and addition is commutative, such as the real numbers.
More concisely: For any linearly ordered additive commutative group `α`, `- (min a b) = max (-a, -b)`.
|