inv_le_of_inv_le'
theorem inv_le_of_inv_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]
[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_le_of_inv_le'` is a generalized assertion about the inverses in a group with a partial ordering. Specifically, for any type `α` that forms a group with a less-than-or-equal-to (`≤`) operator and satisfies certain covariance conditions, if the inverse of an element `a` is less than or equal to another element `b`, then the inverse of `b` is less than or equal to `a`. The covariance conditions ensure that multiplication and the `≤` relation interact in a compatible way.
More concisely: If `α` is a type with a group structure and a reflexive, transitive, and total `≤` relation satisfying the right and left cancellation laws, then for all `a b` in `α`, if `a ≤ b` implies `b⁻¹ ≤ a⁻¹`, then the `≤` relation is a group homomorphism from `(α, ≤)` to `(α, ≤)`.
|
le_neg
theorem 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_neg` states that for any type `α` which forms an additive group and has a less than or equal to (`≤`) relation, such that this `≤` relation is preserved under addition and swapping arguments of the addition (these properties are captured by the `CovariantClass` requirements), then for any two elements `a` and `b` from `α`, `a` is less than or equal to the negation of `b` if and only if `b` is less than or equal to the negation of `a`.
More concisely: For any additive group type `α` equipped with a covariant `≤` relation preserving addition and swapping arguments, `a ≤ -b` if and only if `b ≤ -a`.
|
neg_le
theorem neg_le :
∀ {α : 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 `neg_le` establishes a relationship between the negations of two elements of a type `α`. This type `α` is a member of the `AddGroup` class, which means it has addition and subtraction operations, and it's also a member of the `LE` class, meaning that it has a less-or-equal-to operation. The theorem also requires two covariant classes: one for the regular addition operation and one for the swapped addition operation. Both of these classes also have a less-or-equal-to operation.
The theorem states that for any two elements `a` and `b` of type `α`, `-a` is less than or equal to `b` if and only if `-b` is less than or equal to `a`. In other words, the negation of `a` is less or equal to `b` if the negation of `b` is less or equal to `a`, and vice versa.
More concisely: For all `α` in `AddGroup` and `LE` classes, and for all `a` and `b` in `α`, `-a ≤ b` if and only if `-b ≤ a`.
|
le_inv_of_le_inv
theorem le_inv_of_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]
[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_inv_of_le_inv` is an alias of the forward direction of `le_inv'`. It states that for any given type `α` that forms a Group and has a Less than or Equal to (`LE`) order, that respects both left and right multiplication (due to the `CovariantClass` instances), if an element `a` of this type is less than or equal to the inverse of another element `b`, then `b` is less than or equal to the inverse of `a`.
More concisely: If `a` is less than or equal to the inverse of `b` in a group with a covariant order, then `b` is less than or equal to the inverse of `a`.
|