lt_add_of_sub_right_lt
theorem lt_add_of_sub_right_lt :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
a - c < b → a < b + c
The theorem `lt_add_of_sub_right_lt` states the following principle for any type `α` that has the structure of an additive group and a less than operation: if the operation is covariant, meaning that for any elements `x`, `x_1` of type `α`, swapping the order of addition and then applying the less than operation is equivalent to applying the less than operation directly, then for any three elements `a`, `b`, `c` of type `α`, if `a - c` is less than `b`, then `a` is less than `b + c`. This is essentially an alias of the forward direction of `sub_lt_iff_lt_add` theorem in Lean 4.
More concisely: If `α` is an additive group with a covariant less than relation, then `a < b` implies `a - c < b + c` for all `a, b, c` in `α`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.51
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.51 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
(0 < a - b) = (b < a)
The theorem `Mathlib.Algebra.Order.Group.Defs._auxLemma.51` states that for any type `α` that forms an additive group and has an order relation, and for which adding elements is a covariant operation with respect to the order, the statement "zero is less than the difference of `a` and `b`" is equivalent to the statement "`b` is less than `a`". In more mathematical terms, this theorem says that for all `a` and `b` in `α`, `0 < a - b` if and only if `b < a`.
More concisely: For an additive group type `α` with covariant addition and order relation, `0 < a - b` if and only if `b < a`.
|
Left.inv_lt_one_iff
theorem Left.inv_lt_one_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α}, a⁻¹ < 1 ↔ 1 < a
This theorem, `Left.inv_lt_one_iff`, states that for any type `α` that forms a group and has a less than (`<`) operation, and for any given element `a` of this type `α`, the inverse of `a` is less than 1 if and only if 1 is less than `a`. This relies on the `CovariantClass` property of `α` which, for this theorem, asserts that multiplying elements in `α` preserves the less than relation. In mathematical notation, this would be expressed as: for all `a` in `α`, `a⁻¹ < 1` is equivalent to `1 < a`.
More concisely: For any group type `α` with a `<` relation, the inverse of an element `a` is less than 1 if and only if 1 is less than `a`. (Assuming the `<` relation is covariant.)
|
Left.neg_pos_iff
theorem Left.neg_pos_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, 0 < -a ↔ a < 0
This theorem, named `Left.neg_pos_iff`, states that for any type `α`, assuming it is an additive group and has a defined 'less than' operation such that it is left-covariant (i.e., the operation respects the order when an element is added on the left), then a negative `a` is greater than zero if and only if `a` is less than zero. In simpler terms, it is stating that a number is negative if and only if its negation is positive, under the assumptions of `α` being an additive group with a left-covariant 'less than' operation.
More concisely: For any additive group type `α` with a left-covariant 'less than' relation, `a < 0` if and only if `-a > 0`.
|
lt_add_of_sub_left_lt
theorem lt_add_of_sub_left_lt :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, a - b < c → a < b + c
This theorem states that for any type `α` that forms an Additive Commutative Group and has a less than (`<`) operation satisfying the Covariant Class property, given any three elements `a`, `b` and `c` of `α`, if `a - b` is less than `c`, then `a` is less than `b + c`. In mathematical terms, this theorem captures the fact that adding `b` to both sides of the inequality `a - b < c` gives `a < b + c`.
More concisely: For any additive commutative group type `α` with a Covariant Class `<` operation, if `a - b < c`, then `a < b + c`.
|
LinearOrderedAddCommGroup.compare_eq_compareOfLessAndEq
theorem LinearOrderedAddCommGroup.compare_eq_compareOfLessAndEq :
∀ {α : Type u} [self : LinearOrderedAddCommGroup α] (a b : α), compare a b = compareOfLessAndEq a b
The theorem `LinearOrderedAddCommGroup.compare_eq_compareOfLessAndEq` states that for any type `α` which forms a linear ordered additive commutative group, the comparison of two elements `a` and `b` of `α` using the `compare` method is equivalent to the comparison using the `compareOfLessAndEq` method, given that less than (`<`) and equality (`=`) operations are decidable. In other words, the ordering assigned by the standard comparison and `compareOfLessAndEq` are the same when `α` is a linear ordered additive commutative group.
More concisely: For any type `α` that is a linear ordered additive commutative group with decidable less-than and equality relations, the comparison of elements `a` and `b` using `compare` is equal to the comparison using `compareOfLessAndEq`.
|
le_sub_iff_add_le'
theorem le_sub_iff_add_le' :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, b ≤ c - a ↔ a + b ≤ c
This theorem states that, for any type `α` that forms an additive commutative group and has a less than or equal to (`≤`) relation, which is covariant with respect to addition, if we are given three elements `a`, `b`, and `c` of this type, then `b` is less than or equal to `c - a` if and only if `a + b` is less than or equal to `c`. This theorem provides an equivalence between two ways of expressing a relation between `a`, `b`, and `c`, essentially stating that subtracting `a` from `c` before comparing to `b` is the same as adding `a` to `b` before comparing to `c`.
More concisely: For any additive commutative group `α` with a covariant `≤` relation, `b ≤ c - a` if and only if `a + b ≤ c`.
|
MonotoneOn.neg
theorem MonotoneOn.neg :
∀ {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst_1 : Preorder α]
[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] [inst_4 : Preorder β]
{f : β → α} {s : Set β}, MonotoneOn f s → AntitoneOn (fun x => -f x) s
This theorem states that for any type `α` and `β`, where `α` is an additive group and a preorder, and `β` is a preorder, if you have a function `f` from `β` to `α` that is monotone on a set `s`, then the function that maps each element in `s` to the negation of its image under `f` is antitone on `s`. In other words, if `f` preserves the order of elements in `s`, then the function `-f` reverses it.
More concisely: For functions `f` from a preorder `β` to an additive group and preorder `α` with `f` being monotone on a set `s` in `β`, the function `-f` is antitone on `s`.
|
lt_sub_right_of_add_lt
theorem lt_sub_right_of_add_lt :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
a + b < c → a < c - b
This theorem, `lt_sub_right_of_add_lt`, states that for any type `α` which is an add group (i.e., it supports addition, zero element and inverse operations) and has an order relation `<`, and for which the order is preserved under the operation of adding an element to the right (this property is expressed by the `CovariantClass` instance), if `a + b` is less than `c` (where `a`, `b`, and `c` are elements of this type `α`), then `a` is less than `c - b`. In other words, this theorem provides a condition under which we can subtract `b` from both sides of an inequality and preserve the direction of the inequality.
More concisely: If `α` is an add group with covariant order relation `<` such that `a < c` implies `a + b < c`, then `a < c - b`.
|
Right.one_lt_inv_iff
theorem Right.one_lt_inv_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α},
1 < a⁻¹ ↔ a < 1
The theorem `Right.one_lt_inv_iff` is a statement about a type `α` that has a group structure and an order. The theorem states that for every element `a` of the type `α`, `1` is less than the inverse of `a` if and only if `a` is less than `1`. This is expressed under the condition that `α` forms a covariant class under multiplication by the `swap` function, which swaps the order of multiplication, and the less-than relation. In other words, the theorem establishes a relationship between the ordering of an element and its inverse in a right covariant multiplicative group.
More concisely: In a right covariant group with order relation, an element `a` has `1` as its inverse if and only if `a` is less than `1`.
|
le_one_of_one_le_inv
theorem le_one_of_one_le_inv :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α}, 1 ≤ a⁻¹ → a ≤ 1
This theorem, `le_one_of_one_le_inv`, is an alias of the forward direction of `Left.one_le_inv_iff`. It states that for any type `α` which is a group and has a less than or equal to (`≤`) relation, and for all elements `a` of type `α`, if `1` is less than or equal to the inverse of `a`, then `a` is less than or equal to `1`. The multiplication operation (`*`) in the group is assumed to be left-covariant, meaning that if `x ≤ y`, then `z * x ≤ z * y` for any `z`.
More concisely: If a group element `a` has an inverse such that `1 ≤ its inverse`, then `a ≤ 1`.
|
sub_nonneg_of_le
theorem sub_nonneg_of_le :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
b ≤ a → 0 ≤ a - b
The theorem named `sub_nonneg_of_le` states that for any type `α` that has the structure of an additive group, and for which addition is a covariant operation with respect to an order relation on `α`, if `b` is less than or equal to `a`, then `a - b` is nonnegative, i.e., `0 ≤ a - b`. Here, `a` and `b` are elements of the type `α`. In mathematical notation this is equivalent to the statement: ∀a,b ∈ α, if b ≤ a then 0 ≤ a - b.
More concisely: For any additive group type `α` with covariant addition and order relation, if `b` is less than or equal to `a`, then `a - b` is nonnegative. In mathematical notation: `∀a, b: α, b ≤ a → 0 ≤ a - b`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.10
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.10 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, (0 < -a) = (a < 0)
This theorem, `Mathlib.Algebra.Order.Group.Defs._auxLemma.10`, states that for any type `α` that forms an additive group, is ordered, and satisfies the covariant property, the inequality `0 < -a` is equivalent to `a < 0` for any element `a` of `α`. In other words, a number `a` is negative if and only if `-a` is positive in this context.
More concisely: For any additive group α that is ordered and satisfies the covariant property, the inequality -a < 0 is equivalent to a > 0.
|
sub_le_iff_le_add'
theorem sub_le_iff_le_add' :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a - b ≤ c ↔ a ≤ b + c
This theorem, `sub_le_iff_le_add'`, states that for any type `α` that forms an additive commutative group and has a less than or equal to (`≤`) relation satisfying the covariant property, given any three elements `a`, `b`, and `c` of this type, the statement "the difference between `a` and `b` is less than or equal to `c`" is equivalent to the statement "`a` is less than or equal to the sum of `b` and `c`". In short, it encapsulates the relationship between subtraction and addition in the context of inequalities.
More concisely: For any additive commutative group type `α` with covariant `≤` relation, `a ≤ b + c` is equivalent to `a - b ≤ c`.
|
neg_nonpos_of_nonneg
theorem neg_nonpos_of_nonneg : ∀ {α : Type u} [inst : OrderedAddCommGroup α] {a : α}, 0 ≤ a → -a ≤ 0
This theorem, `neg_nonpos_of_nonneg`, states that for all types `α` that form an ordered additive commutative group, if a given element `a` of type `α` is non-negative (i.e., `a` is greater than or equal to 0), then the negation of `a` (denoted as `-a`) is less than or equal to 0. In other words, if a number is non-negative, its negative counterpart will be non-positive.
More concisely: For all additive, commutative groups with ordering `α`, if `a` is non-negative then `-a` is non-positive.
|
inv_of_one_lt_inv
theorem inv_of_one_lt_inv :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α}, 1 < a⁻¹ → a < 1
This theorem, `inv_of_one_lt_inv`, is essentially an alias for the forward direction of `Left.one_lt_inv_iff`. It works on a type `α` which has an associated group structure and a less than (`<`) operation. Moreover, it assumes the left covariant property on multiplication and less than operation. Given an element `a` of this type `α`, the theorem states that if the reciprocal of `a` (denoted as `a⁻¹`) is greater than 1, then `a` itself must be less than 1.
More concisely: If `α` is a type with a group structure and a total order such that multiplication and the order are left covariant, then for all `a` in `α`, if `1 < a⁻¹`, then `0 < a`.
|
Right.one_le_inv_iff
theorem Right.one_le_inv_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α},
1 ≤ a⁻¹ ↔ a ≤ 1
This theorem, named "Right.one_le_inv_iff", states that for any type `α` that forms a Group and has a less than or equal to (`≤`) operation, and also has a covariant class with respect to multiplication and the `≤` operation using the `Function.swap` function, the following equivalence holds: "1 is less than or equal to the inverse of `a` if and only if `a` is less than or equal to 1". Here, `a` is any element of the type `α`. Essentially, it describes a property of ordered groups, specifically the relationship between an element and its inverse in relation to the multiplicative identity (1).
More concisely: In a group with a type `α` that has a `≤` operation and is covariant with respect to multiplication and `≤` using `Function.swap`, the element 1 is less than or equal to the inverse of any element `a` if and only if `a` is less than or equal to 1.
|
inv_lt_one_iff_one_lt
theorem inv_lt_one_iff_one_lt :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α}, a⁻¹ < 1 ↔ 1 < a
This theorem, named `inv_lt_one_iff_one_lt`, states a property in the context of a group structure with a less-than order relation. Specifically, for any type `α` that has a group structure (where multiplication and inversion operations are defined) and a less-than order (`LT`) relation, the theorem states that the inverse of an element `a` being less than one is equivalent to one being less than `a` itself. This property holds when multiplication is a covariant operation with respect to the less-than order.
More concisely: For any type `α` with a group structure and a covariant less-than order relation `LT`, `a LT one <-> one < a`.
|
OrderedCommGroup.lt_of_mul_lt_mul_left
theorem OrderedCommGroup.lt_of_mul_lt_mul_left :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α]
[inst_2 : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α},
a * b < a * c → b < c
This theorem, `OrderedCommGroup.lt_of_mul_lt_mul_left`, is an alias of `lt_of_mul_lt_mul_left`. It states that for any type `α` equipped with a multiplication operation, a less-than relation, and a contravariant relationship between multiplication and the less-than operation, if the product of `a` and `b` is less than the product of `a` and `c`, then `b` is less than `c`. Essentially, it's a property about the order preservation in the context of multiplication in a commutative ordered group.
More concisely: If `α` is a commutative ordered group, then for all `a`, `b`, and `c` in `α`, if `a * b` < `a * c`, then `b` < `c`.
|
le_inv_mul_of_mul_le
theorem le_inv_mul_of_mul_le :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a * b ≤ c → b ≤ a⁻¹ * c
This theorem, `le_inv_mul_of_mul_le`, states that for any group `α` with a partial order `≤` that is covariant under multiplication, if `a * b ≤ c` for elements `a`, `b`, `c` of `α`, then `b ≤ a⁻¹ * c`. Essentially, this is expressing a property related to cancelling elements in inequalities within the context of a group with a specific order relationship.
More concisely: If `a`, `b`, `c` are elements of a group `α` with a covariant order `≤`, then `a * b ≤ c` implies `b ≤ a⁻¹ * c`.
|
sub_nonpos_of_le
theorem sub_nonpos_of_le :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
a ≤ b → a - b ≤ 0
The theorem `sub_nonpos_of_le` states that for any type `α` that forms an additive group and has a less than or equal to (`≤`) relation, and for which the relation is covariant with respect to the operation of adding two elements of the type, if `a` and `b` are two elements of `α` such that `a` is less than or equal to `b`, then the difference `a - b` is less than or equal to zero. This is an alias of the reverse direction of the theorem `sub_nonpos`. Essentially, if `a` is less than or equal to `b`, then `a - b` is nonpositive.
More concisely: For any additive group type `α` with a covariant `≤` relation, if `a ≤ b`, then `a - b ≤ 0`.
|
le_sub_iff_add_le
theorem le_sub_iff_add_le :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a ≤ c - b ↔ a + b ≤ c
This theorem, `le_sub_iff_add_le`, states that for any type `α` that forms an additive group and has a partial order `≤` satisfying certain properties, and for any elements `a`, `b`, `c` of this type, `a` is less than or equal to `c - b` if and only if `a + b` is less than or equal to `c`. In other words, the theorem establishes an equivalence between the condition of `a` being at most `c - b` and the condition of `a + b` being at most `c`. This theorem embodies a fundamental property of ordered additive groups.
More concisely: For any additive group with partial order `≤` having the property that `a ≤ b` implies `a + c ≤ b + c`, we have `a ≤ c - b` if and only if `a + b ≤ c`.
|
sub_neg
theorem sub_neg :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
a - b < 0 ↔ a < b
The theorem `sub_neg` states that for any type `α` that forms an additive group, has an order `<`, and satisfies the covariance property where swapping the arguments of the addition operation preserves the order, the difference `a - b` of any two elements `a` and `b` of `α` is negative if and only if `a` is less than `b`. In other words, in such a context, subtracting a larger number from a smaller one yields a negative result.
More concisely: For any additive group type `α` with ordering `<` satisfying the covariance property, `a - b` is negative if and only if `a` is less than `b`.
|
neg_pos_of_neg
theorem neg_pos_of_neg :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, a < 0 → 0 < -a
This theorem states that for any type `α` that forms an additive group and has a less-than (`<`) relation, and if this less-than relation is compatible with addition (i.e., it's a covariant class), then for any element `a` of `α`, if `a` is less than zero, then the negation of `a` (i.e., `-a`) is greater than zero. In other words, it confirms the intuitive notion that the negative of a negative number is a positive number.
More concisely: For any additive group type `α` with a covariant `<` relation, if `a` is an element of `α` with `a < 0`, then `-a > 0`.
|
one_le_of_inv_le_one
theorem one_le_of_inv_le_one :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α}, a⁻¹ ≤ 1 → 1 ≤ a
This theorem, named `one_le_of_inv_le_one`, states that for any type `α` that is a group and has a less-than-or-equal-to (`LE`) operation, and where multiplication (`*`) is covariant, if the inverse (`⁻¹`) of an element `a` is less than or equal to `1`, then `1` is less than or equal to `a`. This is also an alias of the forward direction of the `Left.inv_le_one_iff` theorem, indicating that it's a specific case or a re-statement of that theorem.
More concisely: If `α` is a group with a `LE` operation where multiplication is covariant, then `1 ≤ a` holds if and only if `a⁻¹ ≤ 1`. (This is the forward direction of `Left.inv_le_one_iff` theorem.)
|
lt_neg
theorem lt_neg :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[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 : α},
a < -b ↔ b < -a
This theorem is stating a property about less than ("<") relation in an additive group. Specifically, if we have an additive group `α` and two elements `a` and `b` from this group, then `a` is less than the negation of `b` (`a < -b`) if and only if `b` is less than the negation of `a` (`b < -a`). The theorem assumes two conditions on the additive group:
1. It is covariant, meaning that for all elements `x` and `x_1` in the group, the sum of `x` and `x_1` is less than the sum of `x_1` and `x` (`x + x_1 < x_1 + x`).
2. It also has the property that swapping the order of addition preserves the less than relation, i.e., for all `x` and `x_1` in the group, `x + x_1 < x_1 + x` implies `x_1 + x < x + x_1`.
These conditions are captured in Lean 4 by the `CovariantClass` instances `inst_2` and `inst_3`.
More concisely: In an additive group with the covariant property and the commutative property of the less than relation, `a < -b` if and only if `b < -a`.
|
neg_le_neg_iff
theorem neg_le_neg_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[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 : α},
-a ≤ -b ↔ b ≤ a
This theorem, named `neg_le_neg_iff`, asserts a property about the relationship between the negatives of elements in an additive group. Specifically, given a type `α` that forms an additive group (`AddGroup α`) and an order relation (`LE α`), under the assumption that this type follows certain covariance properties (`CovariantClass`), for any two elements `a` and `b` of this type, the negative of `a` is less or equal to the negative of `b` if and only if `b` is less or equal to `a`. The covariance properties are related to the combination of addition and the order relation and their "swapped" versions.
More concisely: For all additive groups `α` with order relation `LE`, and under the assumption of covariance properties, `-a ≤ -b` if and only if `b ≤ a`.
|
sub_le_sub_left
theorem sub_le_sub_left :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[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 : α},
a ≤ b → ∀ (c : α), c - b ≤ c - a
This theorem, named `sub_le_sub_left`, states that for any type `α` which is an additive group and has a less than or equal to (`≤`) relation, if `α` also satisfies two covariant properties involving addition and the `≤` relation, then for any elements `a` and `b` of `α` where `a` is less than or equal to `b`, the difference of any element `c` and `b` is always less than or equal to the difference of `c` and `a`. This is a property related to the order-preserving nature of subtraction in such a mathematical structure.
More concisely: For any additive group `α` with a `≤` relation, if `a ≤ b` implies `a + c ≤ b + c` for all `c` in `α`, then the difference `(c - b) ≤ (c - a)` for all `c` in `α` when `a leq b`.
|
add_lt_of_lt_sub_left
theorem add_lt_of_lt_sub_left :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, b < c - a → a + b < c
The theorem `add_lt_of_lt_sub_left` states that for any additive commutative group `α` with a less-than relation, if `b` is less than the difference of `c` and `a` (`b < c - a`), then the sum of `a` and `b` is less than `c` (`a + b < c`). It's essentially a property of ordered groups, and this version deals with the case where addition is covariant (meaning the order is preserved under addition).
More concisely: If `a`, `b`, and `c` are elements of an additive commutative group with a less-than relation, and `b` is less than the difference between `c` and `a` (`b < c - a`), then `a + b` is less than `c` (`a + b < c`).
|
one_lt_inv_of_inv
theorem one_lt_inv_of_inv :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α}, a < 1 → 1 < a⁻¹
This theorem, named `one_lt_inv_of_inv`, states that for any type `α` which forms a Group and has a less than (`<`) operation, and is covariant with multiplication and the less than operation, if a given element `a` of the group is less than `1`, then the inverse of `a` is greater than `1`. This is an alias for the reverse direction of the theorem `Left.one_lt_inv_iff`.
More concisely: For any group `α` with a covariant `<` operation, if `a` is in `α` and `1 < a`, then `1 < a⁻¹`.
|
sub_right_lt_of_lt_add
theorem sub_right_lt_of_lt_add :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
a < b + c → a - c < b
This theorem, named `sub_right_lt_of_lt_add`, states that for any type `α` that has an addition operation (`AddGroup`), a less than operation (`LT`), and satisfies the `CovariantClass` properties with respect to addition and the less-than relation, given any three elements `a`, `b`, and `c` of type `α`, if `a` is less than the sum of `b` and `c` (`a < b + c`), then the difference of `a` and `c` (`a - c`) is less than `b`. This is essentially a rearrangement property of the inequality involving elements of an additive group.
More concisely: If `a < b + c` in an additive group `α` with `LT` and `AddGroup` structures, then `a - c < b`.
|
neg_neg_of_pos
theorem neg_neg_of_pos : ∀ {α : Type u} [inst : OrderedAddCommGroup α] {a : α}, 0 < a → -a < 0
This theorem, `neg_neg_of_pos`, states that for any type `α` that is an ordered additive commutative group, if a particular element `a` of this type is greater than zero, then the negative of `a` is less than zero. This essentially captures the intuitive idea in mathematics that if a number is positive, its negative is negative, in the context of an ordered additive commutative group.
More concisely: For any ordered additive commutative group `α` and positive element `a` in `α`, `-a` is negative.
|
lt_of_inv_lt_inv
theorem lt_of_inv_lt_inv :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[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 : α},
a⁻¹ < b⁻¹ → b < a
The theorem `lt_of_inv_lt_inv` states that for any type `α` that is a group and has an order (`<`), if this order is compatible with the group operation (`*`) in both directions, then for any elements `a` and `b` of type `α`, if the inverse of `a` is less than the inverse of `b`, then `b` is less than `a`. This theorem can be seen as a version of the mathematical fact that in ordered groups, the order of elements reverses when taking inverses.
More concisely: In an ordered group, if the inverse of one element is less than the inverse of another, then the other element is less than the first.
|
sub_left_lt_of_lt_add
theorem sub_left_lt_of_lt_add :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, a < b + c → a - b < c
This theorem, `sub_left_lt_of_lt_add`, states that for any type `α` that forms an additive commutative group and has a less than relation `<` compatible with addition, given three elements `a`, `b` and `c` of this type, if `a` is less than the sum of `b` and `c` (`a < b + c`), then the difference of `a` and `b` (`a - b`) is less than `c`. This is essentially a rearrangement theorem, expressing the inequality `a < b + c` in a different form.
More concisely: If `a < b + c` in an additive commutative group, then `a - b < c`.
|
add_le_of_le_sub_right
theorem add_le_of_le_sub_right :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a ≤ c - b → a + b ≤ c
The theorem `add_le_of_le_sub_right` is an alias for the forward direction of the theorem `le_sub_iff_add_le`. It states that for any type `α` that forms an additive group and has an order relation such that addition is monotonically increasing in its second argument, if `a` is less than or equal to the difference of `c` and `b` (`a ≤ c - b`), then the sum of `a` and `b` is less than or equal to `c` (`a + b ≤ c`). This provides a useful property for dealing with inequalities in the context of ordered additive groups.
More concisely: If `a` is less than or equal to the difference between `c` and `b` in an additive group with a monotonically increasing order relation, then `a + b` is less than or equal to `c`.
|
inv_mul_lt_iff_lt_mul
theorem inv_mul_lt_iff_lt_mul :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α}, b⁻¹ * a < c ↔ a < b * c
This theorem, `inv_mul_lt_iff_lt_mul`, expresses a property of multiplication in a group with a certain order. Specifically, for all elements `a`, `b`, and `c` of some type `α` which forms a group and has an order (`<`), the statement that `b⁻¹ * a` is less than `c` is equivalent to the statement that `a` is less than `b * c`. This equivalence holds true under the assumption that the multiplication operation `*` of the group is left covariant with respect to the order `<`.
More concisely: In a group with a total order, the multiplicative inverses commute with respect to the order, that is, for all `a, b, c` in the group, `b^-1 * a < c` is equivalent to `a < b * c` if and only if multiplication is left covariant with respect to the order.
|
neg_nonneg_of_nonpos
theorem neg_nonneg_of_nonpos : ∀ {α : Type u} [inst : OrderedAddCommGroup α] {a : α}, a ≤ 0 → 0 ≤ -a
This theorem states that for any type `α` that is an ordered additive commutative group, if an element `a` of this type is less than or equal to zero, then the negation of `a` is greater than or equal to zero. In other words, it's saying that if a number is non-positive, then its negation is non-negative. This is a fundamental property in ordered groups related to the sign reversal of inequalities.
More concisely: For any ordered additive commutative group type `α`, if `a : α` is non-positive, then `-a` is non-negative.
|
sub_le_sub_right
theorem sub_le_sub_right :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
a ≤ b → ∀ (c : α), a - c ≤ b - c
This theorem, "sub_le_sub_right", states that for any type `α` that is an additive group and has a less-than-or-equal-to (`≤`) operation, satisfying the covariance condition with respect to addition, if `a` and `b` are elements of `α` with `a` less than or equal to `b`, then for any other element `c` of `α`, the subtraction of `c` from `a` is less than or equal to the subtraction of `c` from `b`. In common mathematical notation, this could be stated as: if $a \leq b$, then $a - c \leq b - c$ for all $c$ in the additive group $\alpha$.
More concisely: If `α` is an additive group with a covariant `≤` operation, then for all `a ≤ b` in `α` and any `c` in `α`, we have `a - c ≤ b - c`.
|
inv_mul_lt_of_lt_mul
theorem inv_mul_lt_of_lt_mul :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α}, a < b * c → b⁻¹ * a < c
This theorem, `inv_mul_lt_of_lt_mul`, is an alias of the reverse direction of the theorem `inv_mul_lt_iff_lt_mul` in the context of group theory. Given any type `α` that is a group and has a less than (`<`) operation, and that also satisfies the covariant property (where multiplication 'respects' the less than operation), for any elements `a`, `b`, and `c` of this type, if `a` is less than the product of `b` and `c`, then the product of the inverse of `b` and `a` is less than `c`.
More concisely: If `a < b * c` in a group with covariant multiplication, then `c < b ^-1 * a`.
|
neg_add_le_iff_le_add
theorem neg_add_le_iff_le_add :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, -b + a ≤ c ↔ a ≤ b + c
This theorem, `neg_add_le_iff_le_add`, states that for all types `α` that have an addition operation (`AddGroup`), a less-than-or-equal-to relation (`LE`), and satisfy the `CovariantClass` (which in this case means that addition respects the less-than-or-equal-to relation), the inequality `-b + a ≤ c` is equivalent to `a ≤ b + c`. In other words, given any three elements `a`, `b`, and `c` of such a type `α`, subtracting `b` from `a` and checking if the result is less than or equal to `c` is the same as checking if `a` is less than or equal to the sum of `b` and `c`.
More concisely: For all types `α` with `AddGroup`, `LE`, and `CovariantClass` structures, `-b + a ≤ c` if and only if `a ≤ b + c`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.3
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.3 :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α}, (1 ≤ a⁻¹) = (a ≤ 1)
This theorem states that for any type `α` that is a group and has an order defined on it, and that this order is covariant with the group operation, for any element `a` of this type, the condition that `1` is less than or equal to the inverse of `a` holds if and only if `a` is less than or equal to `1`. In this context, 'covariant' means that if `x ≤ y` then `z * x ≤ z * y` for all `z`.
More concisely: For any group `α` with a covariant order `≤` on it, an element `a` has `1 ≤ a⁻¹` if and only if `a ≤ 1`.
|
sub_lt_self
theorem sub_lt_self :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α}, 0 < b → a - b < a
This theorem, `sub_lt_self`, states that for any type `α` that is an additive group and has a less than (`<`) operation, if the operation is covariant, then for any element `a` in `α` and any `b` in `α` such that `b` is greater than 0, the difference of `a` and `b` is strictly less than `a`. In simpler terms, within a certain mathematical structure, subtracting a positive quantity from a number results in a value that's smaller than the original number.
More concisely: For any additive group type `α` with a covariant `<` operation, for all `a` in `α` and positive `b` in `α`, `a - b` is strictly less than `a`.
|
neg_le_self
theorem neg_le_self :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 ≤ a → -a ≤ a
This theorem, referred to as `neg_le_self`, states that for any type `α` which is an additive group and has a preorder relation that is covariant with addition, if `0` is less than or equal to a particular `a` of type `α`, then the negation of `a` is less than or equal to `a`. In other words, for any element `a` in such a structure, if `a` is non-negative, its negative or opposite is always less than or equal to `a`.
More concisely: For any additive group `α` with a covariant preorder relation and any `a` in `α` such that `0 ≤ a`, we have `-a ≤ a`.
|
inv_lt_one'
theorem inv_lt_one' :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α}, a⁻¹ < 1 ↔ 1 < a
This theorem, `inv_lt_one'`, states that for any type `α` that has a group structure and a less-than operation (`<`), and that satisfies the covariant property for multiplication and the less-than operation, the inverse of an element `a` from `α` is less than one if and only if one is less than `a`. In other words, in this set-up, an element `a` is greater than one if and only if its inverse is less than one.
More concisely: For any group with a less-than order relation that is covariant for multiplication, if `a` is an element with `1 < a` then `0 < a⁻¹`.
|
neg_pos
theorem neg_pos :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, 0 < -a ↔ a < 0
This theorem, `neg_pos`, states that for any type `α` which is an additive group and has a less-than (`<`) operation satisfying the covariant property with respect to addition, the statement 'zero is less than negative `a`' is equivalent to 'a is less than zero'. In other words, for any element `a` in such a type `α`, `0 < -a` if and only if `a < 0`.
More concisely: For any additive group `α` with a covariant `<` relation on it, `0 < -a` if and only if `a < 0`.
|
LinearOrderedAddCommGroup.le_total
theorem LinearOrderedAddCommGroup.le_total :
∀ {α : Type u} [self : LinearOrderedAddCommGroup α] (a b : α), a ≤ b ∨ b ≤ a
This theorem states that for any linear ordered additive commutative group, given any two elements `a` and `b` from the group, either `a` is less than or equal to `b`, or `b` is less than or equal to `a`. In other words, the order relation on the group is total, meaning that for any two elements in the group, one is always less than or equal to the other.
More concisely: In any linear ordered additive commutative group, for all elements a and b, either a ≤ b or b ≤ a.
|
sub_le_sub_iff_right
theorem sub_le_sub_iff_right :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α} (c : α),
a - c ≤ b - c ↔ a ≤ b
This theorem, `sub_le_sub_iff_right`, states that for any type `α` which forms an additive group and has a partial order `≤`, where the order respects addition (i.e., is a Covariant Class), given any three elements `a`, `b`, and `c` of type `α`, the inequality `a - c ≤ b - c` holds if and only if `a ≤ b`. In layman's terms, it simply means that subtracting the same number `c` from two numbers `a` and `b` does not change the order of the two numbers.
More concisely: For any additive group type `α` with a covariant partial order `≤`, the subtraction `a - c ≤ b - c` holds if and only if `a ≤ b`.
|
le_sub_right_of_add_le
theorem le_sub_right_of_add_le :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a + b ≤ c → a ≤ c - b
The theorem `le_sub_right_of_add_le` states that for any additive group `α` with a `≤` relation that satisfies the covariant property, given three elements `a`, `b`, `c` of `α`, if `a + b` is less than or equal to `c`, it implies that `a` is less than or equal to `c - b`. This theorem is essentially an alias of the reverse direction of the theorem `le_sub_iff_add_le`.
More concisely: If `a`, `b` are elements of an additive group `α` with a covariant `≤` relation, then `a ≤ c - b` whenever `a + b ≤ c`.
|
OrderedAddCommGroup.to_contravariantClass_right_le
theorem OrderedAddCommGroup.to_contravariantClass_right_le :
∀ (α : Type u) [inst : OrderedAddCommGroup α],
ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
This theorem states that for any type `α` that has an instance of an `OrderedAddCommGroup`, there exists a `ContravariantClass` for the pair `(α, α)` with the `Function.swap` of the binary function `x + x_1` as the co-variant relation and the less than or equal to (`≤`) relation as the contra-variant. In other words, it is saying that the addition operation in an ordered commutative group is contravariant with respect to the order relation. This serves as a choice-free shortcut instance in certain theorem bases involving ordered commutative groups and contravariant relationships.
More concisely: For any ordered commutative group `α`, the addition operation is contravariant with respect to the order relation `≤`, i.e., `x ≤ x_1` implies `x_1 + x ≤ x_1 + x_1`.
|
LinearOrderedAddCommGroup.min_def
theorem LinearOrderedAddCommGroup.min_def :
∀ {α : Type u} [self : LinearOrderedAddCommGroup α] (a b : α), min a b = if a ≤ b then a else b
This theorem states that for any linearly ordered additive commutative group, the minimum function behaves in a certain way. Specifically, for any two elements `a` and `b` in this group, the minimum value between `a` and `b` is equal to `a` if `a` is less than or equal to `b`, and `b` otherwise.
More concisely: For any linearly ordered additive commutative group, the minimum function satisfies `min a b = a if a ≤ b else b`.
|
Left.one_le_inv_iff
theorem Left.one_le_inv_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α}, 1 ≤ a⁻¹ ↔ a ≤ 1
This theorem, named `Left.one_le_inv_iff`, is applicable in the context of a group of elements of type α with a less-than-or-equal ordering and a left covariant operation (multiplication in this case). The theorem states that for any element `a` of the group, `1` is less than or equal to the inverse of `a` if and only if `a` is less than or equal to `1`. In other words, the statement captures a specific order-reversing property of the group inverse operation.
More concisely: In a group with a left covariant operation and a total ordering, the element 1 is less than or equal to the inverse of an element if and only if the element is less than or equal to 1.
|
sub_pos
theorem sub_pos :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
0 < a - b ↔ b < a
This theorem, named `sub_pos`, states that, for any type `α` that has an addition operation (determined by `AddGroup α`), a less than relation (`LT α`), and the operation `+` and relation `<` are compatible with each other (ensured by `CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1`), the difference of two elements `a` and `b` (represented as `a - b`) is greater than zero if and only if `b` is less than `a`. This theorem is a formal statement of a common property of ordered groups.
More concisely: For any additive group `α`, if `a` and `b` are its elements with `a > b`, then `a - b > 0`.
|
lt_inv_of_lt_inv
theorem lt_inv_of_lt_inv :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[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 : α},
a < b⁻¹ → b < a⁻¹
This is a theorem about a property of elements in a group with an order relation. In particular, it states that for any type `α` that forms a group with a less than (`<`) relation and satisfies certain covariance properties, if an element `a` is less than the inverse of another element `b` (i.e., `a < b⁻¹`), then `b` is less than the inverse of `a` (i.e., `b < a⁻¹`). Here, the `CovariantClass` instances ensure that the group operation and the order relation interact in a specific, compatible way.
More concisely: If `α` is a group with a covariant order relation `<` such that `a < b⁻¹` implies `b < a⁻¹`, then the order relation is covariant with respect to group inversion in `α`.
|
LinearOrderedCommGroup.compare_eq_compareOfLessAndEq
theorem LinearOrderedCommGroup.compare_eq_compareOfLessAndEq :
∀ {α : Type u} [self : LinearOrderedCommGroup α] (a b : α), compare a b = compareOfLessAndEq a b
This theorem states that for any linear ordered commutative group (denoted by `α`), the `compare` function's result is equivalent to the result of the `compareOfLessAndEq` function. Specifically, for any two elements `a` and `b` from this group, both functions will yield the same `Ordering` outcome. The `compare` function is defined in the context of the linear ordered commutative group, and `compareOfLessAndEq` is defined using the less-than (`<`) operator and the equality (`=`) operator, which are assumed to be decidable.
More concisely: For any linear ordered commutative group `α`, the `compare` function and the `compareOfLessAndEq` function defined using the less-than (`<`) and equality (`=`) operators agree on their outputs for all elements `a` and `b` from `α`.
|
sub_lt_self_iff
theorem sub_lt_self_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α}, a - b < a ↔ 0 < b
This theorem, `sub_lt_self_iff`, states that for any type `α` that has an addition operation (`AddGroup`), a less-than operation (`LT`), and satisfies the CovariantClass property with respect to addition and less-than operation, for any two elements of this type `a` and `b`, the statement "a minus b is less than a" is equivalent to "0 is less than b". This theorem is a useful property in the domain of ordered groups, where subtraction, addition, and comparison interact.
More concisely: For any additive group `α` with `LT`, we have `a - b < a iff 0 < b`.
|
Right.neg_neg_iff
theorem Right.neg_neg_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, -a < 0 ↔ 0 < a
The theorem `Right.neg_neg_iff` states that for any type `α` that has an addition operation (i.e., an `AddGroup`), a less than operation (i.e., `LT`), and satisfies a certain covariance property specified by `Function.swap fun x x_1 => x + x_1` and `fun x x_1 => x < x_1`, for any element `a` of type `α`, the negation of `a` is less than zero if and only if zero is less than `a`. In other words, it establishes an equivalence between `-a < 0` and `0 < a` under the given conditions.
More concisely: For any type `α` with an `AddGroup` structure, `LT` relation, and satisfying the given covariance property, the negation of an element `a` is less than zero if and only if zero is less than `a`.
|
inv_lt_inv_iff
theorem inv_lt_inv_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[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 : α},
a⁻¹ < b⁻¹ ↔ b < a
This theorem states that for any type `α` which forms a group and has a less-than (`<`) operation that is compatible with its multiplication, and where multiplication is covariant in both arguments, the inverse of an element `a` is less than the inverse of another element `b` if and only if `b` is less than `a`. In mathematical terms, for all `a` and `b` in the group `α`, `a⁻¹ < b⁻¹` is equivalent to `b < a`.
More concisely: For any group `α` with a compatible `<` relation, where multiplication is covariant, the inverse of a smaller element is smaller than the inverse of a larger element: `a < b` if and only if `a⁻¹ > b⁻¹`. (Note: The original statement has been slightly adjusted for clarity and to use the more common notation of `<` for "less than" and `>` for "greater than" with respect to the inverse elements.)
|
sub_lt_sub_left
theorem sub_lt_sub_left :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[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 : α},
a < b → ∀ (c : α), c - b < c - a
The theorem `sub_lt_sub_left` states that for any type `α` that forms an additive group and has a less-than operation, which also satisfies the covariant properties pertaining to both addition and the less-than operation, if `a` and `b` are elements of `α` such that `a < b`, then for every element `c` of `α`, `c - b` is less than `c - a`. In other words, if `a` is less than `b`, subtracting `b` from any number `c` will result in a value less than that obtained by subtracting `a` from `c`. This is similar to the property of real numbers where if `a < b`, then for every `c`, we have `c - b < c - a`.
More concisely: For all additive groups with a covariant less-than relation, if `a < b`, then for all `c`, `c - b < c - a`.
|
sub_le_sub_iff_left
theorem sub_le_sub_iff_left :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[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] {b c : α} (a : α),
a - b ≤ a - c ↔ c ≤ b
This theorem states that for any type `α` that has an addition group structure, a partial ordering (`LE`), and satisfies two covariance properties (one for addition and one for its swapped version), the following inequality holds: subtracting `b` from `a` is less than or equal to subtracting `c` from `a` if and only if `c` is less than or equal to `b`. Here, `a`, `b`, and `c` are elements of the type `α`. In other words, for all real numbers `a`, `b`, and `c`, `a - b ≤ a - c` is equivalent to `c ≤ b`.
More concisely: For any type `α` with an additive structure, a partial ordering `LE`, and the covariance properties for addition and its swapped version, `a LE b` if and only if `c LE b` implies `a - c LE a - b`.
|
sub_lt_iff_lt_add
theorem sub_lt_iff_lt_add :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
a - c < b ↔ a < b + c
This theorem, `sub_lt_iff_lt_add`, states for any type `α` that is an additive group and has a less than (`<`) relation, and if the addition function `+` for `α` is a covariant class with respect to the less than relation (that is, if `a < b` then for any `c`, `c + a < c + b`), then for any elements `a`, `b`, and `c` of type `α`, the inequality `a - c < b` is equivalent to `a < b + c`. In simpler words, this theorem provides a way to rearrange the terms in one inequality to form another, while maintaining the validity of the inequality.
More concisely: For any additive group `α` with a covariant `<` relation, `a < b` is equivalent to `a - c < b - c` for all `a, b, c` in `α`.
|
neg_le_sub_iff_le_add
theorem neg_le_sub_iff_le_add :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, -b ≤ a - c ↔ c ≤ a + b
This theorem, `neg_le_sub_iff_le_add`, states that for any type `α` that is an additive commutative group and has a less than or equal to (`LE`) order, and for any three elements `a`, `b`, `c` of type `α`, the inequality `-b ≤ a - c` is equivalent to `c ≤ a + b`. Specifically, it means that subtracting `c` from `a` and then ensuring the result is greater or equal to negative `b` is the same as adding `b` to `a` and ensuring the result is greater or equal to `c`. This theorem showcases an important property of ordered additive commutative groups.
More concisely: For any additive commutative group with a `LE` order, the inequality `-b ≤ a - c` is equivalent to `c ≤ a + b`.
|
sub_nonneg
theorem sub_nonneg :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
0 ≤ a - b ↔ b ≤ a
This theorem, named `sub_nonneg`, states that for any type `α` that forms an additive group and has a less than or equal to (`≤`) operation, with a specific covariance property, the difference `a - b` (where `a` and `b` are elements of `α`) is nonnegative (i.e., `0 ≤ a - b`) if and only if `b` is less than or equal to `a` (i.e., `b ≤ a`). This covariance property is expressed by the `Function.swap fun x x_1 => x + x_1` and `fun x x_1 => x ≤ x_1` terms: it requires that swapping the order of the inputs to the addition and the `≤` operator produces the same result. In essence, this theorem formalizes a familiar property from elementary arithmetic: subtracting a smaller number from a larger one yields a nonnegative result.
More concisely: For any additive group type `α` with covariant `≤` operation, `a - b ≥ 0` if and only if `b ≤ a`.
|
lt_of_sub_neg
theorem lt_of_sub_neg :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
a - b < 0 → a < b
This theorem, `lt_of_sub_neg`, is an alias for the forward direction of the theorem `sub_neg`. It establishes a property in the context of an additive group. Specifically, for any type α that forms an additive group and has a less-than (`<`) relation that is covariant with respect to addition, if the difference `a - b` is less than zero, then `a` is less than `b`. In other words, if subtracting `b` from `a` results in a negative number, then `a` must be less than `b`. This theorem is a restatement of the fact that `a - -b = a + b`, which is documented in `sub_neg_eq_add`.
More concisely: If `a - b` is negative in an additive group where the less-than relation is covariant with addition, then `a` is less than `b`.
|
OrderedCommGroup.mul_le_mul_left
theorem OrderedCommGroup.mul_le_mul_left :
∀ {α : Type u} [self : OrderedCommGroup α] (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b
This theorem states that multiplication is monotone in an ordered commutative group. By saying that multiplication is monotone, it means that if we have two elements, 'a' and 'b', in a certain ordered commutative group 'α', and 'a' is less than or equal to 'b', then multiplying any element 'c' from the same group by 'a' will result in a product that is less than or equal to the product of 'c' and 'b'.
More concisely: In an ordered commutative group, if a <= b, then for all c in the group, ac <= bc.
|
sub_lt_iff_lt_add'
theorem sub_lt_iff_lt_add' :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, a - b < c ↔ a < b + c
The theorem `sub_lt_iff_lt_add'` states that for any type `α` that has an addition operation (`AddCommGroup`), a less than operation (`LT`), and respects the variant class rule for addition (`CovariantClass`), given any three elements `a`, `b`, and `c` of type `α`, the inequality `a - b < c` is equivalent to `a < b + c`. This captures a basic property of ordered additive groups.
More concisely: For any additive group type `α` with a covariant less-than relation, we have `a - b < c` if and only if `a < b + c`.
|
lt_or_lt_of_sub_lt_sub
theorem lt_or_lt_of_sub_lt_sub :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a - d < b - c → a < b ∨ c < d
This theorem states that for any type `α` that is an additive commutative group and has a linear order and a covariant class, given four elements `a`, `b`, `c`, and `d` of type `α`, if the difference of `a` and `d` is less than the difference of `b` and `c`, then either `a` is less than `b` or `c` is less than `d`. This is a fundamental property that holds in any ordered group.
More concisely: In an additive commutative group equipped with a linear order and a covariant class, if `a ≤ b + c` and `c ≤ d`, then `a ≤ b` or `b ≤ d`.
|
le_of_sub_nonpos
theorem le_of_sub_nonpos :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
a - b ≤ 0 → a ≤ b
The theorem `le_of_sub_nonpos` is an alias for the forward direction of `sub_nonpos` in Lean 4.
This theorem states that for all types `α` that form an additive group and have a defined less than or equal to (`≤`) operation, if the difference `a - b` is less than or equal to zero, then `a` is less than or equal to `b`. This requires the `CovariantClass` property, which in this context means that if adding two elements `x` and `x_1` increases (or doesn't decrease) the value, then `x` is less than or equal to `x_1`. This theorem is true for any two elements `a` and `b` of type `α`.
More concisely: For all additive types `α` with a defined `≤` operation, if `a ≤ b` implies `a - b ≤ 0`, then `a ≤ b`.
|
sub_nonpos
theorem sub_nonpos :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
a - b ≤ 0 ↔ a ≤ b
This theorem, `sub_nonpos`, states that for any type `α` that forms an additive group and has an order relation satisfying the covariance property (specifically, the function that adds two elements of `α` and the less than or equal to relation are covariant), the subtraction of two elements `b` from `a` (denoted as `a - b`) is less than or equal to zero if and only if `a` is less than or equal to `b`. In other words, for all elements `a` and `b` in such a type `α`, `a - b ≤ 0` is equivalent to `a ≤ b`.
More concisely: For every additive group type `α` with a covariant order relation, the subtraction of two elements `a` and `b` satisfies `a - b ≤ 0` if and only if `a ≤ b`.
|
neg_lt_neg
theorem neg_lt_neg : ∀ {α : Type u} [inst : OrderedAddCommGroup α] {a b : α}, a < b → -b < -a
This theorem, `neg_lt_neg`, states that for any type `α` that belongs to the ordered additive commutative group, given two elements `a` and `b` of this type, if `a` is less than `b`, then `-b` is less than `-a`. In other words, it expresses that in the context of an ordered additive commutative group, negating the elements reverses the order relation.
More concisely: For all ordered additive commutative groups (α, <) and elements a, b ∈ α, if a < b then -b < -a.
|
one_lt_of_inv_lt_one
theorem one_lt_of_inv_lt_one :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α}, a⁻¹ < 1 → 1 < a
This theorem, `one_lt_of_inv_lt_one`, states that for any type `α` that has a group structure and an order `<`, the product of two elements of `α` is a new element which is smaller than the two initial elements. Specifically, if the inverse of an element `a` is less than one, then `a` is greater than one. This theorem is an alias of the forward direction of `Left.inv_lt_one_iff`.
More concisely: If `α` is a type with a group structure and an order `<`, and the inverse of an element `a` is less than one, then `a` is greater than one.
|
add_lt_of_lt_sub_right
theorem add_lt_of_lt_sub_right :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
a < c - b → a + b < c
The theorem `add_lt_of_lt_sub_right` states that for any type `α` that is an additive group (`AddGroup α`) and has a less-than relation (`LT α`), and also satisfies the particular covariance condition (`CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1`), if an element `a` of this type `α` is less than the difference of two other elements `c` and `b` (`a < c - b`), then the sum of `a` and `b` is less than `c` (`a + b < c`). In mathematical terms, if $a < c - b$, then $a + b < c$ for elements $a$, $b$, and $c$ of an additive group that supports subtraction and the less-than operation.
More concisely: If $a$ is less than the difference $c-b$ in an additive group with subtraction and a compatible less-than relation, then $a+b$ is less than $c$.
|
lt_mul_of_inv_mul_lt_left
theorem lt_mul_of_inv_mul_lt_left :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α}, b⁻¹ * a < c → a < b * c
This theorem, `lt_mul_of_inv_mul_lt_left`, states that for any group structure `α` with a defined multiplication operation and order, and given three elements `a`, `b`, and `c` of this group, if the product of the inverse of `b` and `a` is less than `c`, then `a` is less than the product of `b` and `c`. It is an alias of the forward direction of the theorem `inv_mul_lt_iff_lt_mul`.
More concisely: If the product of the inverse of `b` and `a` is less than `c` in a group with order, then `a` is less than the product of `b` and `c`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.33
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.33 :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[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 : α},
(a⁻¹ ≤ b⁻¹) = (b ≤ a)
This theorem, named `_auxLemma.33` in the `Mathlib.Algebra.Order.Group.Defs` namespace, states that for any type `α` that forms a group and is partially ordered (with `≤` as the order relation), and satisfies the two specified covariance properties with respect to multiplication and the order relation, for any two elements `a` and `b` of type `α`, the statement "`a` inverse is less than or equal to `b` inverse" is equivalent to the statement "`b` is less than or equal to `a`". In mathematical terms, for any group $(\alpha, *, \leq)$ with covariance properties, $(a^{-1} \leq b^{-1})$ if and only if $(b \leq a)$ for all $a,b \in \alpha$.
More concisely: For any group with covariance properties with respect to multiplication and order relation, `a`'s inverse is less than or equal to `b`'s inverse if and only if `b` is less than or equal to `a`.
|
le_of_sub_nonneg
theorem le_of_sub_nonneg :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
0 ≤ a - b → b ≤ a
The theorem `le_of_sub_nonneg` states that for any type `α` equipped with an addition operation (forming an 'AddGroup'), an order relation (denoted by `≤`), and satisfying the CovariantClass condition (which in this case ensures that "if `x ≤ y` then for all `z`, `z + x ≤ z + y`"), if `a` and `b` are elements of type `α` such that `0 ≤ a - b`, then it must be the case that `b ≤ a`. In other words, if `a - b` is nonnegative, then `a` is greater than or equal to `b`. This is essentially the forward direction of the `sub_nonneg` theorem: "nonnegativity of subtraction implies the order relation".
More concisely: If `α` is an AddGroup with order relation `≤` satisfying CovariantClass condition, and `0 ≤ a - b` for elements `a, b` of `α`, then `b ≤ a`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.44
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.44 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
(0 ≤ a - b) = (b ≤ a)
This theorem, `Mathlib.Algebra.Order.Group.Defs._auxLemma.44`, states that for any type `α` which forms an additive group and has a partial order, if `α` also satisfies the covariance property under the operation of swapping arguments of addition (i.e., Function.swap applied to the addition function) and the less than or equal to ordering, then for any two elements `a` and `b` of type `α`, the statement "zero is less than or equal to the difference of `a` and `b`" is equivalent to the statement "`b` is less than or equal to `a`". In other words, `b ≤ a` if and only if `0 ≤ a - b`.
More concisely: For an additive group `α` with a partial order, if swapping arguments preserves both the group operation and the ordering, then `b ≤ a` if and only if `0 ≤ a - b`.
|
LinearOrderedCommGroup.le_total
theorem LinearOrderedCommGroup.le_total : ∀ {α : Type u} [self : LinearOrderedCommGroup α] (a b : α), a ≤ b ∨ b ≤ a
This theorem states that for any given type `α`, which is a Linear Ordered Commutative Group, and for any two elements `a` and `b` of type `α`, either `a` is less than or equal to `b`, or `b` is less than or equal to `a`. This is essentially an assertion of the totality of the order, a key property which distinguishes linear orders from partial orders. In terms of mathematical language, it states that the given order relation forms a total order on the set.
More concisely: For any Linear Ordered Commutative Group `α`, the relation `≤` on `α` is a total order.
|
mul_inv_le_iff_le_mul
theorem mul_inv_le_iff_le_mul :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a * b⁻¹ ≤ c ↔ a ≤ c * b
This theorem, `mul_inv_le_iff_le_mul`, states that for any type `α` that forms a group and has a defined less than or equal to (`≤`) operation, and a certain covariance property, for any three elements `a`, `b`, and `c` of `α`, the statement "the product of `a` and the inverse of `b` is less than or equal to `c`" is equivalent to " `a` is less than or equal to the product of `c` and `b`."
More concisely: For any group type `α` with a `≤` operation satisfying a covariance property, `a ≤ c * b` if and only if `a * b^(-1) ≤ c`.
|
OrderedCommGroup.to_contravariantClass_right_le
theorem OrderedCommGroup.to_contravariantClass_right_le :
∀ (α : Type u) [inst : OrderedCommGroup α],
ContravariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
This theorem, `OrderedCommGroup.to_contravariantClass_right_le`, applies to any type `α` which has an `OrderedCommGroup` structure. It states that for this type `α`, the function that multiplies the first argument by the second argument and swaps their order (represented as `Function.swap fun x x_1 => x * x_1`) is contravariant with respect to the less than or equal to relation (`x ≤ x_1`). To put it simply, the theorem asserts that in an ordered commutative group, if the product of two elements, when their order is reversed, respects the order relation, then the function is contravariant.
More concisely: If `α` is an ordered commutative group, then the function `x => x_1 * x` is contravariant with respect to the order relation `x ≤ x_1`.
|
LinearOrderedCommGroup.min_def
theorem LinearOrderedCommGroup.min_def :
∀ {α : Type u} [self : LinearOrderedCommGroup α] (a b : α), min a b = if a ≤ b then a else b
This theorem states that for any type `α` that forms a linearly ordered commutative group, the minimum function `min` behaves equivalently to a function obtained from a conditional comparison `minOfLe`. More specifically, given two elements `a` and `b` of type `α`, the minimum of `a` and `b` (`min a b`) is defined to be `a` if `a` is less than or equal to `b` (`a ≤ b`), otherwise it is `b`.
More concisely: For any linearly ordered commutative group type `α`, the function `min` is equivalent to the conditional comparison `minOfLe` such that `min a b = a if a ≤ b else b`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.39
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.39 :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[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 : α},
(a⁻¹ < b⁻¹) = (b < a)
This theorem states that for any type `α` that forms a group and is ordered under a less-than relation (`<`), if this type also satisfies two covariance properties with respect to multiplication and the less-than relation, then for any two elements `a` and `b` of this type, `a` is less than `b` if and only if the inverse of `b` is less than the inverse of `a`. In mathematical notation, this can be written as `(a⁻¹ < b⁻¹) = (b < a)`. The two covariance properties mentioned are properties that relate the order of elements and their multiplication.
More concisely: For any group type `α` ordered by `<`, if multiplication is covariant with respect to the order relation, then `a < b` if and only if `a⁻¹ > b⁻¹`.
|
LinearOrderedAddCommGroup.max_def
theorem LinearOrderedAddCommGroup.max_def :
∀ {α : Type u} [self : LinearOrderedAddCommGroup α] (a b : α), max a b = if a ≤ b then b else a
This theorem states that for any type `α` that forms a `LinearOrderedAddCommGroup`, the maximum value between two elements `a` and `b` is defined as `b` if `a` is less than or equal to `b`, otherwise it is `a`. Here, `LinearOrderedAddCommGroup` is a structure that combines the properties of being an Additive Commutative Group (where addition is commutative and there's an additive inverse for every element) with a linear order (where elements can be compared in a 'less than or equal to' relationship).
More concisely: For any `α` that is a Linear Ordered Additive Commutative Group, the maximum of two elements `a` and `b` is `b` if `a ≤ b`, and `a` otherwise.
|
le_iff_forall_pos_lt_add
theorem le_iff_forall_pos_lt_add :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α},
a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
This theorem states that for any type `α` which has an additive group structure and a linear order, and which satisfies the covariant class condition (i.e., for all `x` and `x_1`, `x + x_1` implies `x ≤ x_1`), a given element `a` is less than or equal to another element `b` if and only if for any positive `ε`, `a` is less than the sum of `b` and `ε`. This theorem essentially characterizes the "less than or equal to" relation in terms of the ability to add a small positive quantity to the larger element to exceed the smaller one.
More concisely: For any additive group `α` with a linear order and covariant class condition, `a ≤ b` if and only if for any positive `ε`, `a + ε ≤ b`.
|
Left.neg_neg_iff
theorem Left.neg_neg_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, -a < 0 ↔ 0 < a
This theorem, named `Left.neg_neg_iff`, states that for any type `α` which is an additive group (`AddGroup α`) and has a less than operation (`LT α`), and wherein addition (`fun x x_1 => x + x_1`) is left-covariant with respect to the less than operation (`fun x x_1 => x < x_1`), a negative value `-a` is less than zero if and only if zero is less than `a`. This theorem uses the left-covariant property and essentially asserts the equivalence of negative values being less than zero and their positive counterparts being greater than zero in the context of an ordered additive group.
More concisely: For any additive group with a total order where addition is left-covariant with respect to the order, the negation of an element is less than zero if and only if zero is less than the element.
|
add_neg_le_neg_add_iff
theorem add_neg_le_neg_add_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[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 c d : α},
a + -b ≤ -d + c ↔ d + a ≤ c + b
The theorem `add_neg_le_neg_add_iff` is a statement about elements in an additive group that is ordered and has certain covariance properties. Specifically, suppose we have an additive group `α`, and four elements `a`, `b`, `c`, `d` in `α`. The theorem states that the inequality `a + -b ≤ -d + c` holds if and only if the inequality `d + a ≤ c + b` holds. This theorem generalizes certain properties of inequalities involving addition and negation in the context of ordered groups.
More concisely: In an ordered additive group, the sum of an element and its negation is less than or equal to the sum of another element and its negation if and only if the second sum is less than or equal to the first.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.2
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.2 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, (-a ≤ 0) = (0 ≤ a)
This theorem, from the Mathlib library in Lean 4, states a property of additive groups with a total order. Specifically, it says that for any element 'a' of such a group, the inequality 'negative a is less than or equal to 0' is equivalent to '0 is less than or equal to a'. This theorem is essentially stating that negating 'a' and comparing it to zero gives the same result as comparing zero to 'a' in the given order structure.
More concisely: For any additive group with a total order, the element 'a' is less than or equal to zero if and only if the negative of 'a' is less than or equal to zero.
|
Right.neg_nonpos_iff
theorem Right.neg_nonpos_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, -a ≤ 0 ↔ 0 ≤ a
The theorem `Right.neg_nonpos_iff` states that for any type `α` that forms an additive group and has a less than or equal to (`≤`) relation, where this relation is compatible with the group operation under swapping of arguments (i.e., it is right covariant), then for any element `a` of this type `α`, `-a` is less than or equal to `0` if and only if `0` is less than or equal to `a`. This theorem essentially captures the property that negating an element reverses its comparison with zero.
More concisely: For any additive group type `α` with a right covariant `≤` relation, `-a ≤ 0` if and only if `0 ≤ a`.
|
lt_or_lt_of_div_lt_div
theorem lt_or_lt_of_div_lt_div :
∀ {α : Type u} [inst : CommGroup α] [inst_1 : LinearOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a / d < b / c → a < b ∨ c < d
This theorem states that for any type `α` that forms a commutative group with a linear order and satisfies the covariant property, if the quotient of `a` and `d` is less than the quotient of `b` and `c`, then `a` is less than `b` or `c` is less than `d`. In mathematical terms, this means that if `a/d < b/c`, then either `a < b` or `c < d`.
More concisely: If `α` is a commutative group with a linear order satisfying the covariant property, then `a < b` or `c < d` holds if and only if `a/d < b/c`.
|
sub_neg_of_lt
theorem sub_neg_of_lt :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
a < b → a - b < 0
This theorem, named `sub_neg_of_lt`, is a variant of the reverse direction of `sub_neg`. It states that for any type `α`, given that `α` has an additive group structure, a less than operation, and satisfies the CovariantClass property with respect to addition and the less than operation, if `a` and `b` are elements of `α` such that `a` is less than `b`, then the difference `a - b` is less than zero. In other words, if `a` is less than `b`, then subtracting `b` from `a` results in a negative number. The equivalent statement in traditional mathematical notation would be: "for all a, b in some additive group, if a < b, then a - b < 0".
More concisely: If `α` is an additive group with a total order such that the order is covariant with respect to addition, then for all `a` and `b` in `α` with `a < b`, it holds that `a - b` is negative.
|
neg_nonneg
theorem neg_nonneg :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 ≤ -a ↔ a ≤ 0
The theorem `neg_nonneg` states that for all elements `a` of an additive group `α`, which also have a less-than-or-equal-to operation and satisfy a certain covariance property, `0` is less than or equal to the negation of `a` if and only if `a` is less than or equal to `0`. In other words, an element `a` of the group is non-positive if and only if its negation is non-negative.
More concisely: For all elements `a` in an additive group with a covariance property, `a` is non-positive if and only if -`a` is non-negative.
|
mul_le_of_le_inv_mul
theorem mul_le_of_le_inv_mul :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α}, b ≤ a⁻¹ * c → a * b ≤ c
This theorem, `mul_le_of_le_inv_mul`, states that for any Type `α` where `α` is a Group and has a less than or equal to (`≤`) operation, under certain conditions, if `b` is less than or equal to the product of the inverse of `a` and `c` (i.e., `b ≤ a⁻¹ * c`), then the product of `a` and `b` is less than or equal to `c` (i.e., `a * b ≤ c`). The conditions are that the multiplication operation on `α` is covariant, meaning it preserves the order of elements.
More concisely: If `α` is a group with a covariant multiplication operation, then `a * b ≤ c` holds if and only if `b ≤ a⁻¹ * c`.
|
lt_div_iff_mul_lt
theorem lt_div_iff_mul_lt :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α},
a < c / b ↔ a * b < c
The theorem `lt_div_iff_mul_lt` states that for any type `α` that has a group structure and a less-than (`<`) relation, and any elements `a`, `b`, `c` of `α`, where the multiplication operation on `α` is covariant with respect to the less-than relation, the inequality `a < c / b` is equivalent to `a * b < c`. Essentially, it relates division and multiplication in the context of inequalities, allowing us to rewrite or simplify expressions involving such inequalities.
More concisely: For any type `α` with a group structure and a covariant multiplication with respect to the `<` relation, `a < c / b` if and only if `a * b < c`.
|
lt_sub_left_of_add_lt
theorem lt_sub_left_of_add_lt :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, a + b < c → b < c - a
This theorem, `lt_sub_left_of_add_lt`, is an alias of the reverse direction of the theorem `lt_sub_iff_add_lt'. For any type `α` that is an additive commutative group and has a less-than (`<`) operation, and if the addition operation (`+`) is covariant in both its arguments with respect to the less-than operation, then for any elements `a`, `b`, and `c` of type `α`, if `a + b` is less than `c`, it implies that `b` is less than `c - a`.
More concisely: If `a`, `b`, and `c` are elements of an additive commutative group `α` with covariant addition and `a + b < c`, then `b < c - a`.
|
add_le_of_le_sub_left
theorem add_le_of_le_sub_left :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, b ≤ c - a → a + b ≤ c
This theorem, `add_le_of_le_sub_left`, is an alias for the forward direction of `le_sub_iff_add_le'`. It states that for any type `α` that is an additive commutative group and has a `≤` relation, and for any three elements `a`, `b` and `c` of this type, if `b` is less than or equal to `c - a`, then the sum of `a` and `b` is less than or equal to `c`. The type `α` must also satisfy the CovariantClass property with respect to addition and the `≤` relation.
More concisely: For any additive commutative group `α` with a total order `≤`, if `b ≤ c - a`, then `a + b ≤ c`.
|
div_le_div''
theorem div_le_div'' :
∀ {α : Type u} [inst : CommGroup α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a ≤ b → c ≤ d → a / d ≤ b / c
This theorem, `div_le_div''`, states that for any type `α` that has a commutative group structure and an preorder relation, and for any `α`'s `a`, `b`, `c`, and `d`, if `a` is less than or equal to `b` and `c` is less than or equal to `d`, then the quotient of `a` and `d` is less than or equal to the quotient of `b` and `c`. Here, the preorder and commutative group structures of `α` are essential to make the division and comparison operations well-defined and meaningful. The CovariantClass is a mathematical structure that ensures that certain properties hold when we multiply elements of `α`.
More concisely: For any commutative group `α` with preorder relation, if `a ≤ b` and `c ≤ d` in `α`, then `a / d ≤ b / c`.
|
sub_lt_sub_right
theorem sub_lt_sub_right :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
a < b → ∀ (c : α), a - c < b - c
This theorem, `sub_lt_sub_right`, states that for all types `α` that are additive groups and have a less-than operation `<` and satisfy the covariance property with respect to addition and `<`, given any two elements `a` and `b` of the type `α` where `a` is less than `b`, for any element `c` of the type `α`, the subtraction of `c` from `a` is less than the subtraction of `c` from `b`. It basically asserts that if `a` is less than `b`, then `a - c` is less than `b - c` for all `c` in an additive group with a well-defined less-than operation satisfying certain covariance conditions.
More concisely: For all additive groups with a well-defined less-than operation satisfying covariance conditions, if `a < b`, then `a - c < b - c` for all `c` in the group.
|
mul_lt_of_lt_inv_mul
theorem mul_lt_of_lt_inv_mul :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α}, b < a⁻¹ * c → a * b < c
This theorem, `mul_lt_of_lt_inv_mul`, is an alias of the forward direction of `lt_inv_mul_iff_mul_lt`. It states that for any type `α` that is a group and has an order (`<`), if `b` is less than the product of the inverse of `a` and `c`, then the product of `a` and `b` is less than `c`. The order (`<`) is compatible with the group operation in the sense defined by the `CovariantClass`.
More concisely: If `α` is a group with order `<` compatible with its group operation, and `a` is an element of `α` such that `b < a⁻¹c`, then `ab < c`.
|
lt_inv_mul_of_mul_lt
theorem lt_inv_mul_of_mul_lt :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α}, a * b < c → b < a⁻¹ * c
This theorem, `lt_inv_mul_of_mul_lt`, is an alias for the reverse direction of the theorem `lt_inv_mul_iff_mul_lt`. It states that for any type `α` that is a group and has a less-than (`<`) operation, and that satisfies the covariant property with respect to multiplication, given any three elements `a`, `b`, and `c` of `α`, if the product of `a` and `b` is less than `c`, then `b` is less than the product of the inverse of `a` and `c`.
More concisely: If `α` is a group with a covariant `<` operation and `a`, `b`, `c` are elements of `α` such that `a * b < c`, then `b < a^(-1) * c`.
|
le_div_iff_mul_le
theorem le_div_iff_mul_le :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a ≤ c / b ↔ a * b ≤ c
This theorem, `le_div_iff_mul_le`, is a statement about elements `a`, `b`, and `c` in a group `α` which is also equipped with a less than or equal to relation (`LE`). The theorem states that `a` is less than or equal to the division of `c` by `b` if and only if the product of `a` and `b` is less than or equal to `c`. The group `α` needs to have a certain property, specifically, it should be a `CovariantClass`. This implies that for any two elements `x` and `x_1` in the group, the swapped multiplication operation (`x * x_1` swapped to `x_1 * x`) should preserve the less than or equal to relation. In other words, if `x ≤ x_1`, then `x * x_1 ≤ x_1 * x`.
More concisely: In a CovariantClass group equipped with a less than or equal to relation, `a ≤ b` if and only if `a * b ≤ c`, for some `c` in the group.
|
neg_le_neg
theorem neg_le_neg : ∀ {α : Type u} [inst : OrderedAddCommGroup α] {a b : α}, a ≤ b → -b ≤ -a
This theorem states that for any ordered additive commutative group `α`, and for any two elements `a` and `b` from `α`, if `a` is less than or equal to `b`, then the negation of `b` is less than or equal to the negation of `a`. In other words, it expresses that within this kind of group, inverting the order of elements by taking their negatives also inverts their inequality relation.
More concisely: For any ordered additive commutative group `α`, if `a ≤ b`, then `-b ≤ -a`.
|
inv_lt'
theorem inv_lt' :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[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 : α},
a⁻¹ < b ↔ b⁻¹ < a
The theorem `inv_lt'` is stated as follows in natural language: For all elements `a` and `b` of a group `α`, which is equipped with a multiplication operation and a less-than relation, and for which both the multiplication operation and its swapped version are covariant with this less-than relation, the reciprocal of `a` is less than `b` if and only if the reciprocal of `b` is less than `a`. In other words, in such a group, the order of inverses (reciprocals) reverses the order of the original elements.
More concisely: In a group equipped with a covariant multiplication and less-than relation, the order of inverses is the reverse of the order of the original elements with respect to the less-than relation.
|
sub_le_iff_le_add
theorem sub_le_iff_le_add :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a - c ≤ b ↔ a ≤ b + c
The theorem `sub_le_iff_le_add` states that for any type `α` that has an addition operation (under the AddGroup structure), a less than or equal to (`≤`) relation, and which satisfies the CovariantClass condition with the addition operation and this less than or equal to relation (specifically, the CovariantClass condition for swapped addition), the inequality `a - c ≤ b` is equivalent to `a ≤ b + c`. In simpler terms, it states that in such a structure, subtracting `c` from `a` being less than or equal to `b` is the same as `a` being less than or equal to the sum of `b` and `c`.
More concisely: For types with an AddGroup structure and a CovariantClass relation between addition and the less than or equal to relation, the subtraction `a - c` being less than or equal to `b` is equivalent to `a` being less than or equal to `b + c`.
|
inv_mul_le_of_le_mul
theorem inv_mul_le_of_le_mul :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a ≤ b * c → b⁻¹ * a ≤ c
This theorem, "inv_mul_le_of_le_mul", is essentially an alias of the reverse direction of another theorem, "inv_mul_le_iff_le_mul". It applies to any group structure with a defined less than or equal to order (`LE`), and a covariant class that respects this order in multiplication. Given three elements of such a group, `a`, `b`, and `c`, if `a` is less than or equal to the product of `b` and `c`, then the product of the inverse of `b` and `a` is less than or equal to `c`.
More concisely: If `a` is less than or equal to `b` multiplied by `c` in a group with a defined order, then the inverse of `b` multiplied by `a` is less than or equal to `c`.
|
inv_le_inv_iff
theorem inv_le_inv_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[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 : α},
a⁻¹ ≤ b⁻¹ ↔ b ≤ a
This theorem, `inv_le_inv_iff`, is a statement about inverse elements in a group with a certain type of order relation. Specifically, consider a group `α` equipped with a multiplication operation and a "less than or equal to" (`≤`) relation. Assume that `α` is covariant, which means that the multiplication operation and the order relation interact in a certain way: if `x` and `y` are elements of the group and `x ≤ y`, then for any other element `z`, we have `z * x ≤ z * y`. Also assume that this covariance holds when the multiplication is done in the opposite order: if `x ≤ y`, then `z * x ≤ z * y` for any `z`. Then, the theorem states that for any two elements `a` and `b` in our group, the inverse of `a` is less than or equal to the inverse of `b` if and only if `b` is less than or equal to `a`.
More concisely: In a covariant group equipped with a multiplication operation and a covariant "less than or equal to" relation, the inverse of an element is less than or equal to the inverse of another element if and only if the other element is less than or equal to the first.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.4
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.4 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, (0 ≤ -a) = (a ≤ 0)
This theorem, named `Mathlib.Algebra.Order.Group.Defs._auxLemma.4`, states for any type `α` which is an additive group and ordered in such a way that addition respects the order, for any element `a` of `α`, the statement that 0 is less than or equal to the negation of `a` is equivalent to the statement that `a` is less than or equal to 0. In mathematical notation, this theorem can be expressed as: for all `a` in some ordered additive group `α`, `0 ≤ -a` if and only if `a ≤ 0`.
More concisely: For any ordered additive group `α`, the element `0` is equal to the additive inverse of `a` if and only if `a` is equal to the additive inverse of `0`, i.e., `0 ≤ -a` if and only if `a ≤ 0`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.42
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.42 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α},
(a - b < a) = (0 < b)
The theorem, named `Mathlib.Algebra.Order.Group.Defs._auxLemma.42`, is a statement about ordered additive groups. Specifically, for any type `α` that forms an additive group and has a less-than order relation that is compatible with its addition operation, and given any elements `a` and `b` of such a type, the theorem states that `a - b` being less than `a` is equivalent to `0` being less than `b`. In other words, in this algebraic structure, subtracting a positive number from `a` results in a number that is less than `a`.
More concisely: For any additive group type `α` with a compatible order relation, `a - b < a` is equivalent to `0 < b`.
|
neg_lt_neg_iff
theorem neg_lt_neg_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[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 : α},
-a < -b ↔ b < a
This theorem, `neg_lt_neg_iff`, states that for any type `α` where `α` is an additive group and also obeys certain ordering and covariance properties, the inequality `-a < -b` is equivalent to `b < a` for any elements `a` and `b` of `α`. In other words, this theorem says that negating both sides of an inequality and swapping them preserves the order in this type `α`. The covariance properties are implicitly indicating that the operations and comparisons are compatible in a certain way in the context of this type `α`.
More concisely: For all additive groups `α` with covariance properties, `-a < -b` is equivalent to `b < a`.
|
lt_sub_comm
theorem lt_sub_comm :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, a < b - c ↔ c < b - a
This theorem, `lt_sub_comm`, states that for all types `α` that form an additive commutative group and an ordered set, and for all elements `a`, `b`, and `c` of that type, the statement "a is less than the difference of b and c" is equivalent to the statement "c is less than the difference of b and a". Here the operation of addition and the less than relation are both assumed to be covariant, which in this context means that if you increase the first argument then the result increases.
More concisely: For all additive commutative groups and ordered sets `α`, and all `a`, `b`, `c` in `α`, the inequality `a < b - c` is equivalent to `c < b - a`.
|
lt_sub_iff_add_lt
theorem lt_sub_iff_add_lt :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α},
a < c - b ↔ a + b < c
The theorem `lt_sub_iff_add_lt` is a statement about elements of an additive group of a certain type, which also possess a less-than order relation, and this order relation is covariant with respect to the group's addition operation. Specifically, for any elements `a`, `b`, and `c` of this type, the theorem states that `a` is less than `c` subtract `b` if and only if `a` plus `b` is less than `c`. This essentially means subtracting `b` from `c` on one side of a less-than inequality is the same as adding `b` to `a` on the other side of the inequality.
More concisely: For all elements `a`, `b`, and `c` in an additive group with a covariant less-than order relation, `a < c < b` if and only if `a + b < c`.
|
le_of_neg_le_neg
theorem le_of_neg_le_neg :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[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 : α},
-a ≤ -b → b ≤ a
The theorem `le_of_neg_le_neg` states that for any type `α` that is an additive group and has a total ordering, and where the operations of addition and the order relation are compatible (both in the usual direction and when the arguments are swapped), if negative `a` is less than or equal to negative `b` then `b` is less than or equal to `a`. This is essentially a formal statement of the property of order reversal under negation for real numbers.
More concisely: For all additive groups `α` with a total ordering and compatible operations, `-a ≤ -b` implies `-b ≤ -a`.
|
lt_mul_of_inv_mul_lt
theorem lt_mul_of_inv_mul_lt :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a b c : α}, b⁻¹ * a < c → a < b * c
This theorem, `lt_mul_of_inv_mul_lt`, is simply an alias for the forward direction of another theorem `inv_mul_lt_iff_lt_mul`. It applies to a context where we have a type `α` that has a group structure and an order (`LT α`). The order is compatible with the group operation (`CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1`). Given three elements `a`, `b`, and `c` of this type `α`, the theorem states that if the product of the inverse of `b` and `a` is less than `c` (i.e., `b⁻¹ * a < c`), then `a` is less than the product of `b` and `c` (i.e., `a < b * c`).
More concisely: If `b¹*-1 * a < c` in a group `α` with compatible order relation `LT`, then `a < b * c`.
|
sub_le_comm
theorem sub_le_comm :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a - b ≤ c ↔ a - c ≤ b
This theorem, `sub_le_comm`, states that for all elements `a`, `b`, and `c` of a type `α`, which belongs to an additive commutative group with a specific covariance property and a less than or equal to order, the difference of `a` and `b` being less than or equal to `c` is equivalent to the difference of `a` and `c` being less than or equal to `b`. In mathematical terms, it asserts that for all `a`, `b`, and `c` in the group, `(a - b) ≤ c` if and only if `(a - c) ≤ b`.
More concisely: For all elements `a`, `b`, and `c` in a commutative additive group with a total order, `(a - b) ≤ c` if and only if `(a - c) ≤ b`.
|
sub_lt_zero
theorem sub_lt_zero :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
a - b < 0 ↔ a < b
This theorem, `sub_lt_zero`, states that for any type `α` that forms an additive group, has a less-than operation, and satisfies the covariance property with respect to addition and less-than, for any two elements `a` and `b` of type `α`, the statement "the subtraction of `b` from `a` is less than zero" is equivalent to the statement "`a` is less than `b`". In other words, given all the mentioned conditions, `a - b < 0` if and only if `a < b`.
More concisely: For any additive group type `α` with a covariant less-than relation, `a < b` if and only if `a - b < 0`.
|
neg_add_lt_iff_lt_add
theorem neg_add_lt_iff_lt_add :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, -b + a < c ↔ a < b + c
This theorem states that, for any type `α` that is an additive group and has a less than operation (`LT`), and for any three elements `a`, `b`, and `c` of this type, the inequality `-b + a < c` is equivalent to `a < b + c`. This is specified under the condition that `α` has a CovariantClass with respect to addition and the less than operation, which is a way of saying that `α` behaves in a certain way with respect to these two operations.
More concisely: For any additive group `α` with a less than operation, the inequalities `-b + a < c` and `a < b + c` are equivalent.
|
Right.inv_le_one_iff
theorem Right.inv_le_one_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α},
a⁻¹ ≤ 1 ↔ 1 ≤ a
The theorem `Right.inv_le_one_iff` states that for any type `α` which forms a group and has a less than or equal to (`≤`) relation defined on it, and if `α` has a covariant class defined with the group operation and the `≤` relation, then for any element `a` of `α`, the inverse of `a` is less than or equal to `1` if and only if `1` is less than or equal to `a`. In other words, in such a group, an element and its inverse have a mirrored relationship with respect to `1` in the order defined by `≤`.
More concisely: In a group equipped with a covariant order relation, an element is less than or equal to one if and only if its inverse is.
|
OrderedCommGroup.to_contravariantClass_left_le
theorem OrderedCommGroup.to_contravariantClass_left_le :
∀ (α : Type u) [inst : OrderedCommGroup α], ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1 := by
sorry
This theorem states that for any type `α` which is an Ordered Commutative Group, it is a Contravariant Class under the specific operations. The two operations are multiplication and the less than or equal to relation. In more formal terms, `α` is a Contravariant Class under multiplication for the function `(fun x x_1 => x * x_1)` and the less than or equal to relation for the function `(fun x x_1 => x ≤ x_1)`. This is a key property in order theory that helps establish the relationship between multiplication and the order operation in Ordered Commutative Groups.
More concisely: In an Ordered Commutative Group `α`, multiplication is a contravariant operation with respect to the order relation.
|
inv_lt_of_inv_lt'
theorem inv_lt_of_inv_lt' :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[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 : α},
a⁻¹ < b → b⁻¹ < a
This theorem, `inv_lt_of_inv_lt'`, states that for any type `α` that has a group structure and an order (`LT α`), if the order is compatible with the group operation in both directions (as specified by the `CovariantClass` instances), then for any two elements `a` and `b` of that type, if the inverse of `a` is less than `b`, then the inverse of `b` is less than `a`. In other words, it's a theorem regarding the order of inverses in a group, stating that the order is reversed when taking inverses.
More concisely: If `α` is a type with a covariant group and order structure such that the group operation preserves order in both directions, then for all `a` and `b` in `α`, `a < b` implies `b⁻¹ < a⁻¹`.
|
Left.nonneg_neg_iff
theorem Left.nonneg_neg_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 ≤ -a ↔ a ≤ 0
This theorem, `Left.nonneg_neg_iff`, states for all types `α` that are part of an `AddGroup` and also have a `≤` order defined, with covariance between addition and this order, the non-negativity of the negation of a value `a` is equivalent to `a` being less than or equal to zero. In simpler terms, it provides a condition to check if a certain element `a` is less than or equal to zero in the context of an additive group with a suitable order relation.
More concisely: For types `α` in an additive group with a covariant order `≤` such that `a ≤ 0` if and only if `-a ≥ 0`, the negation of `a` is non-negative if and only if `a` is less than or equal to zero.
|
sub_left_le_of_le_add
theorem sub_left_le_of_le_add :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a ≤ b + c → a - b ≤ c
This theorem, `sub_left_le_of_le_add`, is an alias of the reverse direction of the theorem `sub_le_iff_le_add'` in Lean 4. It states that for any type `α` that is a commutative group under addition and has a less than or equal to (`≤`) relation, and for any three elements `a`, `b`, and `c` of type `α`, if `a` is less than or equal to the sum of `b` and `c`, then the result of subtracting `b` from `a` is less than or equal to `c`.
More concisely: If `a ≤ b + c` in a commutative group with `≤`, then `a - b ≤ c`.
|
sub_le_self
theorem sub_le_self :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α}, 0 ≤ b → a - b ≤ a
This theorem, `sub_le_self`, is essentially an alias for the reverse direction of another theorem, `sub_le_self_iff`. It applies to any type `α` that forms an additive group and has a less-than-or-equal-to (`≤`) operation that is covariant in both arguments. The theorem states that, for any elements `a` and `b` of such a type, if `b` is nonnegative (`0 ≤ b`), then the result of subtracting `b` from `a` (`a - b`) is less than or equal to `a`.
More concisely: For all additive groups with covariant `≤` operation, if `α` has non-negative element `b`, then `a ≤ a - b`.
|
le_sub_left_of_add_le
theorem le_sub_left_of_add_le :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a + b ≤ c → b ≤ c - a
This theorem, named `le_sub_left_of_add_le`, is an alias of the reverse direction of `le_sub_iff_add_le'`. It states that for any type `α` that is an additive commutative group and has a less than or equal to (`LE`) operation, and where addition and the `LE` operation satisfy the covariant property, if `a + b` is less than or equal to `c`, then `b` is less than or equal to `c - a`. In other words, if the sum of two elements is less than or equal to a third, you can subtract the first element from the third and the second element will be less than or equal to the result.
More concisely: If `α` is an additive commutative group with covariant `LE` operation, then `b <= c - a` whenever `a + b <= c`.
|
sub_lt_comm
theorem sub_lt_comm :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, a - b < c ↔ a - c < b
This theorem, `sub_lt_comm`, states that for any type `α` that has an additive commutative group structure and a less than operation (`<`), and that satisfies the covariant class properties with respect to addition and the less than operation, the inequality `a - b < c` holds if and only if `a - c < b` holds for any elements `a`, `b`, `c` in `α`. In other words, it says that subtracting `b` from `a` and testing whether this is less than `c` is equivalent to subtracting `c` from `a` and testing whether this is less than `b`.
More concisely: For any additive commutative group `α` with a covariant `<` relation, `a - b < c` if and only if `a - c < b`.
|
le_sub_comm
theorem le_sub_comm :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a ≤ b - c ↔ c ≤ b - a
This theorem, `le_sub_comm`, states that for any type `α` that forms an additive commutative group and for which less than or equal (`≤`) is defined, and for any three elements `a`, `b`, and `c` of `α`, the statement "`a` is less than or equal to the difference of `b` and `c`" is equivalent to the statement "`c` is less than or equal to the difference of `b` and `a`". This is subject to the condition that the type `α` forms a covariant class under the operation of addition and the less than or equal to relation.
More concisely: For any additive commutative group `α` with defined `≤`, `a ≤ b - c` if and only if `c ≤ b - a`.
|
Left.neg_nonpos_iff
theorem Left.neg_nonpos_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, -a ≤ 0 ↔ 0 ≤ a
This theorem, `Left.neg_nonpos_iff`, declares a fundamental property of ordered additive groups. For any type `α` that has an additive group structure and an order `≤` that is compatible with the group operation (i.e., it is left-covariant), the theorem states that for any element `a` of this type, `-a` is less than or equal to `0` if and only if `0` is less than or equal to `a`. In other words, `a` is nonnegative if and only if its negation `-a` is nonpositive.
More concisely: For any additive group `α` with a compatible ordering `≤`, the elements `a` and `-a` are related by `a ≤ 0 iff -a ≥ 0`.
|
le_add_of_sub_left_le
theorem le_add_of_sub_left_le :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α}, a - b ≤ c → a ≤ b + c
This is an alias for the forward direction of the theorem `sub_le_iff_le_add'`. It states that for any type `α` that is an additive commutative group and has a less-than-or-equal-to (`≤`) relation satisfying some covariance condition, given any three elements `a`, `b`, and `c` of `α`, if `a - b` is less than or equal to `c`, then `a` is less than or equal to `b + c`.
More concisely: For any additive commutative group `α` with covariant `≤` relation, if `a ≤ b + c`, then `a - b ≤ c`.
|
add_neg_le_iff_le_add
theorem add_neg_le_iff_le_add :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a + -b ≤ c ↔ a ≤ c + b
The theorem `add_neg_le_iff_le_add` states that for any type `α` that is an add group and has a less than or equal to (`LE`) operation, and is covariant under the operation of swapping the arguments of addition and the less than or equal to operations, the statement "a plus the additive inverse of b is less than or equal to c" is equivalent to the statement "a is less than or equal to c plus b", for all elements `a`, `b`, `c` of type `α`. In other words, for all elements in an additive group, subtracting a value from one side of an inequality is equivalent to adding that value to the other side.
More concisely: For all elements `a`, `b`, `c` in an additive group with a covariant `LE` operation, `a + (-b) ≤ c` is equivalent to `a ≤ c + b`.
|
neg_lt_iff_pos_add'
theorem neg_lt_iff_pos_add' :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, -a < b ↔ 0 < a + b
This theorem states that for any type `α` that forms an additive group and has a less than (`<`) relation, and for any two elements `a` and `b` of that type, `-a` is less than `b` if and only if `0` is less than the sum of `a` and `b`. The condition `CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1` ensures that the less than relation `<` and the addition operation `+` interact in the way expected for an ordered additive group.
More concisely: For any additive group `α` with a total order, `-a < b` if and only if `0 < a + b`.
|
OrderedCommGroup.le_of_mul_le_mul_left
theorem OrderedCommGroup.le_of_mul_le_mul_left :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α]
[inst_2 : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α},
a * b ≤ a * c → b ≤ c
This theorem, `OrderedCommGroup.le_of_mul_le_mul_left`, states that for any type `α` that has a multiplication operation, a less-than-or-equal-to relation, and a contravariant class (which is a class where multiplication and the less-than-or-equal-to relation interact in a specific way), given any three elements `a`, `b`, `c` of `α`, if the product of `a` and `b` is less than or equal to the product of `a` and `c`, then `b` is less than or equal to `c`. In essence, this is a property of ordered commutative groups where you can compare the ratios of elements.
More concisely: If `α` is an ordered commutative group, then for all `a, b, c` in `α`, if `a * b <= a * c`, then `b <= c`.
|
sub_le_self_iff
theorem sub_le_self_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a : α) {b : α}, a - b ≤ a ↔ 0 ≤ b
This theorem, `sub_le_self_iff`, states that for any type `α` that forms an add group and has an order relation, under the condition that addition is a covariant operation, for any value `a` of such type `α`, the statement "a minus b is less than or equal to a" holds true if and only if "b is greater than or equal to zero". In mathematical terms, it says that for all a and b in α, a - b ≤ a if and only if 0 ≤ b.
More concisely: For any add group type `α` with order relation where addition is covariant, `a ≤ a + b` if and only if `b ≥ 0`.
|
LinearOrderedCommGroup.max_def
theorem LinearOrderedCommGroup.max_def :
∀ {α : Type u} [self : LinearOrderedCommGroup α] (a b : α), max a b = if a ≤ b then b else a
This theorem states that for any linearly ordered commutative group, represented by the type `α`, the maximum between two elements `a` and `b` of this type can be defined as `b` if `a` is less than or equal to `b`, otherwise as `a`. In other words, it's stating that the `max` function is equivalent to choosing the greater element based on the `≤` comparison.
More concisely: For any linearly ordered commutative group `α`, the maximum of two elements `a` and `b` is `a` if `a ≤ b`, and `b` otherwise.
|
one_le_inv'
theorem one_le_inv' :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α}, 1 ≤ a⁻¹ ↔ a ≤ 1
This theorem, `one_le_inv'`, states that for any type `α` that forms a group and has a less than or equal to (`≤`) operation, and also satisfies a certain covariant class property related to multiplication and the `≤` operation, the inverse `a⁻¹` of an element `a` of `α` is greater than or equal to 1 if and only if `a` is less than or equal to 1. This theorem uses the `left` covariant.
More concisely: For any group `α` with a `≤` operation satisfying a certain covariant property, `a≤1` if and only if `1≤a⁻¹`.
|
OrderedCommGroup.mul_lt_mul_left'
theorem OrderedCommGroup.mul_lt_mul_left' :
∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {b c : α},
b < c → ∀ (a : α), a * b < a * c
The theorem `OrderedCommGroup.mul_lt_mul_left'` states that for any type `α` with multiplication and a less than relation, and also satisfying the condition that multiplication preserves the less than relation, if `b` is less than `c`, then for any element `a` of `α`, `a * b` is less than `a * c`. In simpler terms, in a certain kind of ordered group, multiplication on the left preserves the order of elements.
More concisely: In an ordered commutative monoid, if `a` is an element and `b` < `c`, then `a * b` < `a * c`.
|
mul_inv_le_inv_mul_iff
theorem mul_inv_le_inv_mul_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[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 c d : α},
a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b
The theorem `mul_inv_le_inv_mul_iff` states that for any type `α` that forms a group and has a less than or equal to relation (`LE`) defined on it, if it satisfies two specific covariance properties, then for any four elements `a`, `b`, `c` and `d` of this type, the inequality `a * inverse of b` is less than or equal to `inverse of d * c` if and only if `d * a` is less than or equal to `c * b`. Here, `inverse` refers to the inverse operation in the group. The covariance properties are related to the interaction of the multiplication operation and the less than or equal to relation in the group.
More concisely: For all groups α with a defined LE relation, if multiplication is LE-covariant and inverse-preserving, then for all a, b, c, d ∈ α, a * b^-1 ≤ c * d^-1 if and only if d * a ≤ c * b.
|
one_le_div'
theorem one_le_div' :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b : α},
1 ≤ a / b ↔ b ≤ a
This theorem, `one_le_div'`, states that for any type `α` that has a group structure and a less-than-or-equal-to (`≤`) relation, and where the multiplication operation is covariant, for any two elements `a` and `b` of type `α`, `1` is less than or equal to the division of `a` by `b` if and only if `b` is less than or equal to `a`. In other words, if you can meaningfully divide and compare elements in `α`, this theorem relates the ordering of `a` and `b` to the ordering of `1` and `a / b`.
More concisely: For any type `α` with group structure and a `≤` relation where multiplication is covariant, `1 ≤ a / b` if and only if `b ≤ a`.
|
Right.inv_lt_one_iff
theorem Right.inv_lt_one_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α},
a⁻¹ < 1 ↔ 1 < a
The theorem `Right.inv_lt_one_iff` states that for any type `α` that is a group and has a less than (`<`) operation, and is right covariant, meaning that for all elements `x` and `x_1` in `α`, the product `x * x_1` preserves the less than relation when the arguments are swapped, then for any element `a` in `α`, `a⁻¹` is less than `1` if and only if `1` is less than `a`. In mathematical terms, this can be written as ∀a ∈ α, a⁻¹ < 1 ↔ 1 < a.
More concisely: For any right covariant group (α, <) with identity element 1, a^-1 < 1 if and only if 1 < a.
|
Right.neg_pos_iff
theorem Right.neg_pos_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, 0 < -a ↔ a < 0
This theorem, `Right.neg_pos_iff`, states that for any type `α` which is an additive group and has a `<` comparison operator, and assuming that this type has the CovariantClass property with respect to the function that swaps the order of addition, then for any element `a` of type `α`, `0` is less than the negation of `a` if and only if `a` is less than `0`. This is a fundamental theorem related to the properties of negation and order in additive groups.
More concisely: For any additive group type `α` with a `<` comparison operator and the CovariantClass property for swapping addition, `0 < -a` if and only if `a < 0`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.24
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.24 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c : α},
(c ≤ a + -b) = (c + b ≤ a)
This theorem, `Mathlib.Algebra.Order.Group.Defs._auxLemma.24`, is a statement about groups with an order relation, specifically additively written groups (`AddGroup α`) equipped with a less than or equal to relation (`LE α`). The theorem asserts that, for any three elements `a`, `b`, `c` of such a group, the inequality `c ≤ a + -b` is equivalent to `c + b ≤ a`. This essentially expresses the concept of subtracting `b` from both sides of an inequality in the context of an additively written group. The underlying group must also satisfy a certain covariance condition for the less than or equal to relation with respect to the group operation (`CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1`).
More concisely: In an additively written group equipped with a covariant order relation, the inequality `c ≤ a - b` is equivalent to `c + b ≤ a`.
|
sub_le_sub
theorem sub_le_sub :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b c d : α},
a ≤ b → c ≤ d → a - d ≤ b - c
This theorem, `sub_le_sub`, states that in a given additive commutative group, which also has a preorder and a covariant class (where addition is a covariant operation and the order relation is less than or equal to), if one element `a` is less than or equal to another element `b`, and a third element `c` is less than or equal to a fourth element `d`, then the result of `a - d` is guaranteed to be less than or equal to the result of `b - c`. This theorem is a generalized form of the subtraction property of inequality.
More concisely: In an additive commutative group with a covariant preorder relation, if a ≤ b and c ≤ d, then a - d ≤ b - c.
|
lt_sub_iff_add_lt'
theorem lt_sub_iff_add_lt' :
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, b < c - a ↔ a + b < c
This theorem states that for any type `α` that forms an additive commutative group and has a less than (`<`) operation, and for this addition operation and less than operation, if they satisfy the covariant property, then for any three elements `a`, `b` and `c` in `α`, `b` is less than `c` subtracted by `a` if and only if `a` plus `b` is less than `c`. The covariant property here ensures the "order" is preserved under the addition operation.
More concisely: For any additive commutative group `α` with a covariant `<` relation, if `a < b`, then `a + c < c + b` for all `a, b, c` in `α`.
|
Left.one_lt_inv_iff
theorem Left.one_lt_inv_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α}, 1 < a⁻¹ ↔ a < 1
This theorem, `Left.one_lt_inv_iff`, states that for any type `α` that forms a group with a less than (`<`) operation and satisfies a specific covariance condition, a certain element `a` of this group satisfies the inequality `1 < a⁻¹` (1 is less than the inverse of `a`) if and only if `a < 1` (a is less than 1). This theorem shows that in this mathematical structure, being less than 1 and having an inverse greater than 1 are equivalent properties for any element.
More concisely: For any group `α` with a covariant `<` relation, `1 < a` if and only if `a < 1` for all elements `a` in `α`.
|
inv_mul_le_iff_le_mul
theorem inv_mul_le_iff_le_mul :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a b c : α}, b⁻¹ * a ≤ c ↔ a ≤ b * c
This theorem, `inv_mul_le_iff_le_mul`, states that for any type `α` that is a group and has an order (`LE`), and for which multiplication is covariant, given any three elements `a`, `b`, and `c` of that type, the inequality `b⁻¹ * a ≤ c` holds if and only if the inequality `a ≤ b * c` holds. In other words, multiplying `a` by the inverse of `b` is less than or equal to `c` if and only if `a` is less than or equal to the product of `b` and `c`.
More concisely: For any group type `α` with order `LE` and covariant multiplication, the equality `b^(-1) * a ≤ c` is equivalent to `a ≤ b * c`.
|
neg_lt
theorem neg_lt :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[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 : α},
-a < b ↔ -b < a
The theorem `neg_lt` states that for any type `α` that has an additive group structure and an order relation `<` that is covariant with respect to addition (in both the regular and the swapped argument order), for any two elements `a` and `b` of `α`, `-a` is less than `b` if and only if `-b` is less than `a`. Here, `-a` and `-b` denote the additive inverses of `a` and `b`, respectively. The covariance conditions essentially mean that adding the same value to both sides of a `<` inequality does not change the truth of the inequality.
More concisely: For any type `α` with an additive group structure and a covariant order relation `<`, `-a < b` if and only if `-b < a`.
|
OrderedAddCommGroup.add_le_add_left
theorem OrderedAddCommGroup.add_le_add_left :
∀ {α : Type u} [self : OrderedAddCommGroup α] (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b
This theorem states that in an ordered additive commutative group, addition is monotone. More specifically, if you have two elements, `a` and `b`, of some type `α` that forms an ordered additive commutative group, and `a` is less than or equal to `b`, then for any other element `c` of type `α`, the sum `c + a` is less than or equal to the sum `c + b`.
More concisely: In an ordered additive commutative group, if `a` is less than or equal to `b`, then for all `c`, `c + a` is less than or equal to `c + b`.
|
neg_lt_zero
theorem neg_lt_zero :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, -a < 0 ↔ 0 < a
This theorem, `neg_lt_zero`, states that for any type `α` that is an additive group and has a less than (`<`) operation, and where addition and less than operation satisfy the CovariantClass properties, the negative of any element `a` from `α` is less than zero if and only if zero is less than `a`. This establishes a relationship between the negative of a number being less than zero and zero being less than the number itself in this type of mathematical structure.
More concisely: For any additive group type `α` with CovariantClass `<` operation, `-a < 0 <-> 0 < a`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.1
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.1 :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α}, (a⁻¹ ≤ 1) = (1 ≤ a)
This theorem, `Mathlib.Algebra.Order.Group.Defs._auxLemma.1`, asserts that for any type `α` that forms a group and has a less than or equal to (`≤`) operation, and also satisfies the covariant property for multiplication and the less than or equal to operation, then for any element `a` of that type, `a` inverse is less than or equal to `1` if and only if `1` is less than or equal to `a`. In mathematical notation, this theorem can be written as: For all `a` in `α`, `a⁻¹ ≤ 1` if and only if `1 ≤ a`.
More concisely: For any group `α` with a `≤` relation that is covariant for multiplication and left-inverse, `a⁻¹ ≤ 1` if and only if `1 ≤ a`.
|
Left.inv_le_one_iff
theorem Left.inv_le_one_iff :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α}, a⁻¹ ≤ 1 ↔ 1 ≤ a
This theorem, named `Left.inv_le_one_iff`, is applicable to any type `α` that has a group structure and an order relation, and it also assumes that this order is compatible with the group operation in the sense given by the `CovariantClass`. The theorem states that for any element `a` of the group, the inverse of `a` is less than or equal to one if and only if one is less than or equal to `a` itself. It therefore provides a condition in terms of the group inverse operation and the order relation that characterizes when an element is greater than or equal to the identity element of the group.
More concisely: For any group `α` with a compatible order relation, `a` in `α` has an inverse in `α` that is less than or equal to one if and only if one is less than or equal to `a`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.40
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.40 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[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 : α},
(-a < -b) = (b < a)
This theorem, named `Mathlib.Algebra.Order.Group.Defs._auxLemma.40`, states that for any type `α` that is an additive group and has a less-than relation `<`, and which satisfies the 'CovariantClass' properties for both addition and its swapped variant, it is true that for all elements `a` and `b` of that type, `-a` is less than `-b` if and only if `b` is less than `a`.
In simpler terms, within such an additive group, this theorem establishes a relationship between the ordering of two negated elements and the ordering of those same two elements without negation.
More concisely: For any additive group with a covariant ordering, the negation of one element is less than the negation of another if and only if the original elements are ordered opposite to each other.
|
Right.nonneg_neg_iff
theorem Right.nonneg_neg_iff :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 ≤ -a ↔ a ≤ 0
This theorem, `Right.nonneg_neg_iff`, states that for all elements `a` of a type `α`, which is an additive group and has a defined less than or equal to (`LE`) operation, such that the operation is right-covariant (i.e., reversing the order of the operation and then adding doesn't change the order of comparison), the non-negativity of the negation of `a` is equivalent to `a` being less than or equal to zero. In other words, if we have a right-covariant additive group, then `0` is less than or equal to the negation of `a` if and only if `a` is less than or equal to `0`.
More concisely: For all elements `a` in an additive group with right-covariant order relation, `a ≤ 0` if and only if `-a ≤ 0`.
|
inv_le_one'
theorem inv_le_one' :
∀ {α : Type u} [inst : Group α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {a : α}, a⁻¹ ≤ 1 ↔ 1 ≤ a
This theorem, `inv_le_one'`, establishes an equivalence between the statement that the inverse of an element `a` from a group `α` is less than or equal to `1`, and the statement that `1` is less than or equal to `a`. This relationship is valid for any group `α` that is equipped with a less than or equal to (`LE`) relation and satisfies the covariant class property with respect to multiplication and this ordering. The theorem serves as an alias of `Left.inv_le_one_iff` and employs the left covariant property.
More concisely: The theorem `inv_le_one` states that for any group `α` with a `LE` relation satisfying the covariant property, the inverse of an element `a` is less than or equal to 1 if and only if 1 is less than or equal to `a`.
|
sub_pos_of_lt
theorem sub_pos_of_lt :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
b < a → 0 < a - b
This theorem, named `sub_pos_of_lt`, is a variant of the theorem `sub_pos` in the reverse direction. It states that for any type `α` that is an additive group and has an order relation `<`, and a particular covariance property, if `b` is less than `a` (written as `b < a`), then `a - b` is positive (written as `0 < a - b`).
More concisely: If `α` is an additive group with an order relation `<` and `b` is less than `a` in `α`, then `a - b` is positive.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.12
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.12 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, (-a < 0) = (0 < a)
This theorem from Mathlib's Algebraic Order Group Definitions, denoted as `_auxLemma.12`, states that for any type `α` that is an additive group and has an order relation `<` compatible with addition, the inequality `-a < 0` is equivalent to `0 < a` for any element `a` of `α`. In other words, a negative quantity is less than zero if and only if zero is less than the corresponding positive quantity.
More concisely: For any additive group type `α` with a compatible order relation `<`, the inequality `-a < 0` is equivalent to `0 < a`.
|
Mathlib.Algebra.Order.Group.Defs._auxLemma.34
theorem Mathlib.Algebra.Order.Group.Defs._auxLemma.34 :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[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 : α},
(-a ≤ -b) = (b ≤ a)
The theorem `Mathlib.Algebra.Order.Group.Defs._auxLemma.34` states that for any type `α` that is an additive group and has a total order, if the order is compatible with addition in both directions (captured by the `CovariantClass` instances), then for any two elements `a` and `b` of `α`, the inequality `-a ≤ -b` is equivalent to `b ≤ a`.
More concisely: For any additive group with a compatible total order, the inequality -a <= -b holds if and only if b <= a.
|
neg_lt_self
theorem neg_lt_self :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α}, 0 < a → -a < a
The theorem `neg_lt_self` is an alias of `Left.neg_lt_self`. It states that for any type `α`, if `α` is an additive group and has a preorder, and if addition on `α` is covariant, then for any value `a` in `α`, if `0` is less than `a`, then the negative of `a` is less than `a`. In other words, for positive `a`, `-a` is less than `a`.
More concisely: For any additive group `α` with a preorder and covariant addition, if `0 < a` in `α`, then `-a < a`.
|
inv_le_inv'
theorem inv_le_inv' : ∀ {α : Type u} [inst : OrderedCommGroup α] {a b : α}, a ≤ b → b⁻¹ ≤ a⁻¹
This theorem states that for any ordered commutative group `α` and any two elements `a` and `b` of `α`, if `a` is less than or equal to `b`, then the inverse of `b` is less than or equal to the inverse of `a`. In other words, given the inequality `a ≤ b` in the group, we can deduce the inequality `b⁻¹ ≤ a⁻¹`.
More concisely: For any ordered commutative group `α`, if `a ≤ b`, then `b⁻¹ ≤ a⁻¹`.
|
neg_nonpos
theorem neg_nonpos :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, -a ≤ 0 ↔ 0 ≤ a
This theorem, `neg_nonpos`, states that for all types `α` that have an additive group structure and an order `≤` that is compatible with the group operation (in the sense of the `CovariantClass` condition), the negation of a number `a` is non-positive if and only if `a` is non-negative. In mathematical notation, this can be expressed as `-a ≤ 0 ↔ 0 ≤ a`.
More concisely: For all types `α` with an additive group structure and a compatible order, `-a ≤ 0 if and only if 0 ≤ a`.
|
OrderedAddCommGroup.to_contravariantClass_left_le
theorem OrderedAddCommGroup.to_contravariantClass_left_le :
∀ (α : Type u) [inst : OrderedAddCommGroup α], ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
The theorem `OrderedAddCommGroup.to_contravariantClass_left_le` establishes that for any type `α` that has an `OrderedAddCommGroup` structure, the type `α` has a `ContravariantClass` structure with respect to the operation of addition (`fun x x_1 => x + x_1`) and the binary relation of less than or equal to (`fun x x_1 => x ≤ x_1`). In other words, it asserts the invariance of the less than or equal relation under left addition for every ordered additive commutative group.
More concisely: For any ordered additive commutative group `α`, the addition operation and the less than or equal relation define a contravariant class structure on `α`.
|
one_lt_inv'
theorem one_lt_inv' :
∀ {α : Type u} [inst : Group α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α}, 1 < a⁻¹ ↔ a < 1
This theorem is an alias of `Left.one_lt_inv_iff` and it concerns the properties of groups and orderings. Specifically, for any type `α` that forms a group with a less-than relation and a specific covariance property, it states that `1` is less than the inverse of a group element `a` if and only if `a` is less than `1`. This uses the 'left' covariance, that is multiplication on the left.
More concisely: For any group with a left-covariant ordering, `1` is less than the inverse of an element `a` if and only if `a` is less than `1`.
|
lt_of_sub_pos
theorem lt_of_sub_pos :
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α]
[inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α},
0 < a - b → b < a
The theorem `lt_of_sub_pos` states that for any type `α` which is an additive group and has a less than operation `<` that is covariant with the addition operation, if `a` and `b` are elements of `α` and the difference `a - b` is greater than zero, then `b` is less than `a`. In other words, this theorem says that if the subtraction of two elements results in a positive value, the subtracted element is less than the element from which it was subtracted.
More concisely: If `α` is an additive group with a covariant `<` relation such that `a - b > 0` implies `b < a`.
|