max_le_add_of_nonneg
theorem max_le_add_of_nonneg :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddZeroClass α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
0 ≤ a → 0 ≤ b → max a b ≤ a + b
The theorem `max_le_add_of_nonneg` states that for any type `α` equipped with a linear order, the structure of an additive zero class, and the property that addition is covariant in both arguments, if `a` and `b` are elements of `α` and both are nonnegative (i.e., greater than or equal to zero), then the maximum of `a` and `b` is less than or equal to the sum of `a` and `b`. In mathematical symbols, it states that if `0 ≤ a` and `0 ≤ b`, then `max(a, b) ≤ a + b`.
More concisely: For any type with a linear order, additive zero, and covariant addition, if `a` and `b` are nonnegative elements, then `max(a, b) ≤ a + b`.
|
min_add_add_right
theorem min_add_add_right :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b c : α),
min (a + c) (b + c) = min a b + c
The theorem `min_add_add_right` states that for all types `α` which have a linear order and an addition operation (the operation must be covariant, i.e., if `x ≤ y` then `x + z ≤ y + z` for all `z`), the minimum of `a + c` and `b + c` is equal to the minimum of `a` and `b` added to `c`. In mathematical terms, this can be written as: ∀ a, b, c ∈ α, min(a + c, b + c) = min(a, b) + c. It essentially describes a property of the addition operation in a ordered additive structure in the presence of a minimum operation.
More concisely: For all types `α` with a covariant addition and a minimum operation, the minimum of `a + c` and `b + c` equals `min(a, b) + c`.
|
lt_or_lt_of_add_lt_add
theorem lt_or_lt_of_add_lt_add :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a₁ a₂ b₁ b₂ : α},
a₁ + b₁ < a₂ + b₂ → a₁ < a₂ ∨ b₁ < b₂
This theorem, named `lt_or_lt_of_add_lt_add`, states that for any type `α` that has a linear order, an addition operation, and satisfies certain covariance properties, given four elements `a₁, a₂, b₁, b₂` of type `α`, if the sum of `a₁` and `b₁` is less than the sum of `a₂` and `b₂`, then either `a₁` is less than `a₂` or `b₁` is less than `b₂`. In other words, if the sum of two pairs of elements is in a certain order, then at least one element from each pair must also be in that order. The covariance properties ensure that the order and addition operations are compatible in a particular way.
More concisely: If `α` is a type with a linear order and an additive structure satisfying covariance properties, then for all `a₁, a₂, b₁, b₂` in `α`, if `a₁ + b₁ < a₂ + b₂`, then either `a₁ < a₂` or `b₁ < b₂`.
|
lt_or_lt_of_mul_lt_mul
theorem lt_or_lt_of_mul_lt_mul :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_3 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a₁ a₂ b₁ b₂ : α},
a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂
The theorem `lt_or_lt_of_mul_lt_mul` states that for any type `α` that has a linear order and a multiplication operation, and satisfies the covariance property for both multiplication and its swap function (which basically means `α` is an ordered commutative ring), given four elements `a₁`, `a₂`, `b₁`, `b₂` from `α`, if the product of `a₁` and `b₁` is less than the product of `a₂` and `b₂`, then `a₁` is less than `a₂` or `b₁` is less than `b₂`. In simpler terms, given two pairs of numbers, if one pair's product is smaller than the other, then at least one of the components of the smaller pair is less than its corresponding component in the larger pair. This is a formalization of a property of multiplication in ordered commutative rings.
More concisely: In an ordered commutative ring, if a1 * b1 < a2 * b2, then a1 < a2 or b1 < b2.
|
max_add_add_right
theorem max_add_add_right :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b c : α),
max (a + c) (b + c) = max a b + c
The theorem `max_add_add_right` states that for any type `α` that has a linear order and an addition operation, and where the order respects the addition (that is, for any two elements `x` and `x_1` in `α`, if `x` is less than or equal to `x_1`, then `x + y` is less than or equal to `x_1 + y` for any `y` in `α`), then the maximum of `a + c` and `b + c` is equal to the maximum of `a` and `b` plus `c`, for any elements `a`, `b`, and `c` in `α`. In mathematical terms, this theorem is saying that $\max(a + c, b + c) = \max(a, b) + c$ for any numbers `a`, `b`, and `c`, given a numerical type `α` with the properties described.
More concisely: For any type `α` with a linear order and addition operation where `x ≤ x_1` implies `x + y ≤ x_1 + y` for all `x`, `x_1`, and `y` in `α`, the maximum of `a + c` and `b + c` equals the maximum of `a` and `b` plus `c`, for any `a`, `b`, and `c` in `α`. (Or, mathematically: $\max(a + c, b + c) = \max(a, b) + c$ for all `a`, `b`, and `c` in `α`.)
|
min_add_add_left
theorem min_add_add_left :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Add α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b c : α),
min (a + b) (a + c) = a + min b c
This theorem, named `min_add_add_left`, states that for any type `α` that has a linear order, an addition operation, and is a covariant class with respect to addition and the less than or equal to relation, for any three elements `a`, `b`, and `c` of `α`, the minimum of the sums `a + b` and `a + c` is equal to `a` plus the minimum of `b` and `c`. In mathematical terms, it says that $\min(a + b, a + c) = a + \min(b, c)$.
More concisely: For any type `α` with a linear order and covariant addition, the minimum of `a + b` and `a + c` equals `a + min(b, c)` for all elements `a, b, c` in `α`.
|