add_tsub_cancel_left
theorem add_tsub_cancel_left :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
[inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a + b - a = b
This theorem, `add_tsub_cancel_left`, states that for any type `α` that has a partial order, an additive commutative semigroup structure, a subtraction operation, and an ordered subtraction property, and where addition is a contravariant operation with respect to the order, if you have two elements `a` and `b` of this type, then adding `a` to `b` and then subtracting `a` results in `b`. In simple mathematical terms, it can be represented as `a + b - a = b`.
More concisely: For any additive commutative semigroup with subtraction and ordered subtraction property, where addition is contravariant with respect to the order, the order of elements `a` and `b` does not matter, as `a + b = b + a` implies `a + b - a = b`.
|
add_tsub_add_eq_tsub_right
theorem add_tsub_add_eq_tsub_right :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
[inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a c b : α),
a + c - (b + c) = a - b
This theorem states that for any type `α` equipped with a partial order, an additive commutative semigroup structure, a subtraction operation, an ordered subtraction structure, and satisfying both a contravariant and a covariant condition related to addition and order, for any elements `a`, `b`, and `c` of this type `α`, the sum of `a` and `c` subtracted by the sum of `b` and `c` is equal to `a` subtracted by `b`. This is essentially an abstract algebraic formulation of the common arithmetic property that "addition of the same number to both the minuend and subtrahend does not affect the difference".
More concisely: For any type `α` with a partial order, additive commutative semigroup structure, subtraction operation, and ordered subtraction structure, the law of tricommutativity holds: `(a + c) - (b + c) = a - b` for all `a`, `b`, `c` in `α`.
|
add_tsub_le_right
theorem add_tsub_le_right :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
a + b - b ≤ a
The theorem `add_tsub_le_right` establishes that for any type `α` that has a preorder relation, an addition operation, a subtraction operation, and satisfies the `OrderedSub` property, for any two elements `a` and `b` of this type, the result of adding `b` to `a` and then subtracting `b` is less than or equal to `a`. This result holds true in the context of contravariant classes, as indicated by the reference to the `add_tsub_cancel_right` theorem.
More concisely: For any type `α` with a preorder, addition, and subtraction operations satisfying the `OrderedSub` property, `a + b - b ≤ a`.
|
add_tsub_le_assoc
theorem add_tsub_le_assoc :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - c ≤ a + (b - c)
This theorem, `add_tsub_le_assoc`, states that for any type `α` which has an order (`Preorder`), an additive commutative semigroup structure (`AddCommSemigroup`), a subtraction operation (`Sub`), and an ordered subtraction property (`OrderedSub`), and for any three instances `a`, `b`, and `c` of that type `α`, if the addition operation (`fun x x_1 => x + x_1`) respects the order (`fun x x_1 => x ≤ x_1`), then the expression `a + b - c` is always less than or equal to `a + (b - c)`. This theorem thus expresses a specific kind of associativity relation for addition and subtraction operations in this ordered, additive context.
More concisely: For any type `α` with order, additive commutative semigroup structure, subtraction operation, and ordered subtraction property, if addition respects the order, then `a + (b - c)` is the same as `(a + b) - c`, and the former is less than or equal to the latter.
|
AddLECancellable.le_tsub_of_add_le_right
theorem AddLECancellable.le_tsub_of_add_le_right :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α}, AddLECancellable b → a + b ≤ c → a ≤ c - b
The theorem `AddLECancellable.le_tsub_of_add_le_right` states that for any type `α` that has the structure of a preorder, an additive commutative semigroup, and an ordered subtraction, given three elements `a`, `b`, and `c` of `α`, if `b` satisfies the `AddLECancellable` property (which means that for all `b` and `c` in `α`, if `b + a` is less than or equal to `c + a` then `b` is less than or equal to `c`), and if the sum of `a` and `b` is less than or equal to `c`, then `a` is less than or equal to the result of subtracting `b` from `c`. In simpler terms, this theorem gives us a way to compare two elements `a` and `c - b` in a preorder where addition and subtraction interact in a specific way, under certain conditions involving `b`.
More concisely: Given an additive commutative semigroup `α` with an ordered subtraction and an element `b` satisfying `AddLECancellable` property, if `a + b ≤ c` and `b` is less than or equal to `c`, then `a ≤ c - b`.
|
tsub_eq_of_eq_add_rev
theorem tsub_eq_of_eq_add_rev :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α} [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a = b + c → a - b = c
This theorem states that for any type `α` that has a partial order, addition that is commutative, subtraction, and an ordered subtraction operation, and a contravariant class between `α` and the operations of addition and less than or equal to comparison, if `a` is equal to the sum of `b` and `c`, then the result of subtracting `b` from `a` is equal to `c`. The proof of this theorem is omitted.
More concisely: For any type `α` with a commutative addition, subtraction, and a contravariant subtraction relation, if `a = b + c`, then `a - b = c`.
|
Mathlib.Algebra.Order.Sub.Defs._auxLemma.1
theorem Mathlib.Algebra.Order.Sub.Defs._auxLemma.1 :
∀ {α : Type u_1} [inst : LE α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
(a - b ≤ c) = (a ≤ c + b)
This theorem, named `Mathlib.Algebra.Order.Sub.Defs._auxLemma.1`, states that for any type `α` that supports an order (`LE α`), addition (`Add α`), subtraction (`Sub α`), and ordered subtraction (`OrderedSub α`), and for any three elements `a`, `b`, and `c` of type `α`, the inequality `a - b ≤ c` holds true if and only if `a ≤ c + b`. This essentially states a property of ordered subtraction in the context of ordered algebraic structures.
More concisely: For any type `α` with order, addition, subtraction, and ordered subtraction, the subtraction `a - b` is less than or equal to `c` if and only if `a` is less than or equal to `c + b`.
|
AddLECancellable.lt_add_of_tsub_lt_left
theorem AddLECancellable.lt_add_of_tsub_lt_left :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α}, AddLECancellable b → a - b < c → a < b + c
The theorem `AddLECancellable.lt_add_of_tsub_lt_left` states that for any type `α`, under the conditions that `α` is a partially ordered set, an additive commutative semigroup, and has an ordered subtraction operation, and given three elements `a`, `b`, `c` in `α` such that `b` satisfies the `AddLECancellable` property (i.e., for all elements `x` and `y` in `α`, `b + x ≤ b + y` implies `x ≤ y`), if `a - b` is less than `c`, then `a` is less than `b + c`. This theorem represents a property of addition and subtraction in the context of ordered additive structures.
More concisely: If `α` is an ordered additive semigroup with an ordered subtraction operation, and `b` is AddLECancellable, then `a < b + c` given `a - b < c`.
|
le_tsub_of_add_le_left
theorem le_tsub_of_add_le_left :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α} [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a + b ≤ c → b ≤ c - a
This theorem states that for any type `α` that is a preorder, an additive commutative semigroup, and has a subtraction operation that is ordered, and with a contravariant relation between addition and the less-equal relation, if the sum of two elements `a` and `b` is less than or equal to a third element `c`, then `b` is less than or equal to the difference of `c` and `a`. In mathematical notation, this is saying that if $a + b \leq c$, then $b \leq c - a$.
More concisely: If `α` is a preorder, an additive commutative semigroup with ordered subtraction and contravariant addition relation, then for all `a`, `b`, and `c` in `α`, `a + b ≤ c` implies `b ≤ c - a`.
|
tsub_right_comm
theorem tsub_right_comm :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
{a b c : α}, a - b - c = a - c - b
This theorem, `tsub_right_comm`, states that for any type `α` that has a partial order, is an additive commutative semigroup, has a subtraction operation, and respects the order under subtraction, and for any three elements `a`, `b`, and `c` of this type, the difference `a - b - c` is equal to `a - c - b`. In other words, the subtraction operation on the right side of `a` in this type is commutative.
More concisely: For any type with a partial order, additive commutative semigroup structure, and subtraction operation respecting the order, the subtraction operation is right-commutative. That is, for all `a, b, c`, `a - b - c = a - c - b`.
|
tsub_le_iff_left
theorem tsub_le_iff_left :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α}, a - b ≤ c ↔ a ≤ b + c
This theorem, `tsub_le_iff_left`, states that for any type `α` that has a preorder structure, an additive commutative semigroup structure, a subtraction operation, and an ordered subtraction operation, and given any three elements `a`, `b`, and `c` of type `α`, the relation "the difference of `a` and `b` is less than or equal to `c`" is equivalent to the relation " `a` is less than or equal to the sum of `b` and `c`". In LaTeX terms, this states that for all $a, b, c$ in the set `α`, $a - b \leq c$ if and only if $a \leq b + c$.
More concisely: For any type `α` with preorder, additive commutative semigroup, subtraction, and ordered subtraction structures, the subtraction `a - b` is less than or equal to `c` if and only if `a` is less than or equal to the sum `b + c`.
|
antitone_const_tsub
theorem antitone_const_tsub :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {c : α}
[inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], Antitone fun x => c - x
The theorem `antitone_const_tsub` states that for any type `α` that has a preorder structure, an additive commutative semigroup structure, a subtraction operation, and an ordered subtraction, and for any constant `c` of type `α`, the function `f(x) = c - x` is antitone. In other words, if `a ≤ b` for any `a` and `b` of type `α`, then `f(b) = c - b ≤ c - a = f(a)`. This theorem requires that addition on `α` is covariant, meaning that `x + y ≤ x + z` whenever `y ≤ z`.
More concisely: For any type `α` endowed with a preorder, an additive commutative semigroup structure, subtraction, and ordered subtraction, the function `f(x) = c - x` is antitone, i.e., `f(a) ≤ f(b)` whenever `a ≤ b`. Under this setup, `α`'s addition is covariant.
|
AddLECancellable.tsub_eq_of_eq_add
theorem AddLECancellable.tsub_eq_of_eq_add :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α}, AddLECancellable b → a = c + b → a - b = c
The theorem `AddLECancellable.tsub_eq_of_eq_add` states that in the context of a partially ordered additive commutative semigroup with subtraction, which also has the property of ordered subtraction, if an element `b` is 'addition left-cancellable' (meaning that for all elements `b` and `c`, if `b + a ≤ c + a` then `b ≤ c`), and if another element `a` is equal to the sum of `c` and `b`, then the difference `a - b` is equal to `c`. This essentially says that you can 'undo' the addition of a cancellable element by subtracting it.
More concisely: If `a = c + b` in a partially ordered additive commutative semigroup with subtraction and `b` is addition left-cancellable, then `a - b = c`.
|
lt_tsub_iff_left
theorem lt_tsub_iff_left :
∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α]
[inst_3 : OrderedSub α], a < b - c ↔ c + a < b
This theorem `lt_tsub_iff_left` is about linear orders, addition and subtraction in a commutative semigroup. It states that for any type `α` that has a linear order, is an additive commutative semigroup and has a notion of subtraction and an ordered subtraction, the inequality `a < b - c` is equivalent to `c + a < b`. This can also be understood as 'subtracting `c` from `b` and comparing the result with `a` is the same as adding `a` to `c` and comparing the result with `b`'.
More concisely: For any commutative semigroup with additions, subtractions, and a linear order, the inequality `a < b - c` is equivalent to `c + a < b`.
|
eq_tsub_of_add_eq
theorem eq_tsub_of_add_eq :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α} [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + c = b → a = b - c
This theorem states that for any type `α` which is a partially ordered set, an additive commutative semigroup, has a subtraction operation, and has an ordered subtraction property, given three elements `a`, `b`, and `c` of type `α` and satisfying the contravariant property, if `a + c` equals `b`, then `a` is equal to `b` subtract `c`. In other words, if the sum of `a` and `c` is `b`, then `a` is what you get when you subtract `c` from `b`.
More concisely: If `α` is a partially ordered, additive commutative semigroup with subtraction and ordered subtraction property, then for all `a`, `b`, `c` in `α` with `a + c = b`, it follows that `a = b - c`.
|
add_tsub_add_le_tsub_left
theorem add_tsub_add_le_tsub_left :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - (a + c) ≤ b - c
This theorem, `add_tsub_add_le_tsub_left`, says that for all types `α` that are ordered and have operations of addition and subtraction, where addition is both commutative and associative, and the type `α` satisfies the covariant class property, then for any three elements `a`, `b`, and `c` of `α`, the inequality `a + b - (a + c) ≤ b - c` holds. The theorem utilizes properties of ordered sets, addition, subtraction, and covariance.
More concisely: For all types `α` with commutative, associative addition and subtraction, and the covariant class property, the inequality `a + b - a - c ≤ b - c` holds for all elements `a`, `b`, and `c` of `α`.
|
AddLECancellable.add_tsub_cancel_right
theorem AddLECancellable.add_tsub_cancel_right :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b : α}, AddLECancellable b → a + b - b = a
This theorem, named `AddLECancellable.add_tsub_cancel_right`, states that for any type `α` which has a partial order, is an additive commutative semigroup, has subtraction, and ordered subtraction, if an element `b` in `α` is `AddLECancellable`, then adding `b` to any other element `a` in `α` and then subtracting `b` will just give `a`. In other words, if an element `b` is such that adding `b` to any element `x` preserves the order of `x` (that is, if `a + b ≤ a + c` implies `b ≤ c`), then `a + b - b` equals `a` for any `a`. This is a version of the familiar algebraic law that adding a number and then subtracting the same number leaves the original number unchanged, but in a context where the operations may not behave as they do in standard arithmetic.
More concisely: If `α` is a type with a partial order, additive commutative semigroup structure, subtraction, and ordered subtraction, and `b` in `α` is AddLECancellable, then `a + b = a + b - b` for all `a` in `α`.
|
OrderedSub.tsub_le_iff_right
theorem OrderedSub.tsub_le_iff_right :
∀ {α : Type u_3} [inst : LE α] [inst_1 : Add α] [inst_2 : Sub α] [self : OrderedSub α] (a b c : α),
a - b ≤ c ↔ a ≤ c + b
This theorem, `OrderedSub.tsub_le_iff_right`, states that for any type `α` with defined less-than-or-equal-to (`LE`), addition (`Add`), and subtraction (`Sub`) operations, as well as an ordered subtraction property (`OrderedSub`), given any three values `a`, `b`, and `c` of type `α`, `a - b` is less than or equal to `c` if and only if `a` is less than or equal to `c + b`. In other words, the difference between `a` and `b` provides a lower bound on `c` under the condition that `a` is less than or equal to the sum of `c` and `b`.
More concisely: For any type `α` with `LE`, `Add`, and `Sub` operations and ordered subtraction property `OrderedSub`, `a LE c <-> a + b LE c`, where `a`, `b`, and `c` are values of type `α`.
|
tsub_le_tsub
theorem tsub_le_tsub :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c d : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a ≤ b → c ≤ d → a - d ≤ b - c
This theorem, `tsub_le_tsub`, states that for any preorder type `α` that is also an additive commutative semigroup and has subtraction, and is ordered with respect to subtraction, if `a ≤ b` and `c ≤ d`, then `a - d ≤ b - c`. In the context of the theorem, `a`, `b`, `c`, and `d` are elements of the type `α`, and `CovariantClass` is a class that expresses that addition `(fun x x_1 => x + x_1)` is monotonic with respect to the preorder `(fun x x_1 => x ≤ x_1)` on `α`. In simpler words, if `a` is less than or equal to `b`, and `c` is less than or equal to `d`, then the difference of `a` and `d` is less than or equal to the difference of `b` and `c`.
More concisely: If `α` is a preorder type that is an additive commutative semigroup with subtraction and is ordered with respect to subtraction, then for all `a ≤ b` and `c ≤ d` in `α`, we have `a - d ≤ b - c`.
|
AddLECancellable.eq_tsub_of_add_eq
theorem AddLECancellable.eq_tsub_of_add_eq :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α}, AddLECancellable c → a + c = b → a = b - c
The theorem `AddLECancellable.eq_tsub_of_add_eq` states that for any partially ordered commutative semigroup with subtraction that is also an ordered subtraction, given elements `a`, `b`, and `c` such that `c` is left-cancellable with respect to addition, if the sum of `a` and `c` equals `b`, then `a` is equal to the result of subtracting `c` from `b`. In mathematical terms, for all `a`, `b`, `c` in a certain algebraic structure, if `c` has the property that for all `x`, `y`, `c + x ≤ c + y` implies `x ≤ y` and `a + c = b`, then `a = b - c`.
More concisely: If `a`, `b`, and `c` are in a commutative semigroup with subtraction and `c` is left-cancellable for addition, then `a = b - c` whenever `a + c = b`.
|
add_tsub_cancel_right
theorem add_tsub_cancel_right :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
[inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a + b - b = a
The theorem `add_tsub_cancel_right` states that for any type `α` which has a partial order, a commutative semigroup structure under addition, a subtraction operation, an ordered subtraction structure, and a contravariant class structure relating addition to the partial order, subtracting `b` from the sum of `a` and `b` returns `a`. In simple terms, for any two elements `a` and `b` in this type `α`, adding `b` to `a` and then subtracting `b` will leave you with `a` again. This mirrors the intuitive arithmetic property `a + b - b = a`.
More concisely: For any type `α` equipped with a partial order, commutative semigroup structure under addition, subtraction operation, ordered subtraction structure, and contravariant class structure, the law of cancellation holds for right subtraction: `a + b = c + b -> a = c`.
|
add_tsub_add_le_tsub_add_tsub
theorem add_tsub_add_le_tsub_add_tsub :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c d : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a + b - (c + d) ≤ a - c + (b - d)
This theorem states that for any type `α` equipped with a preorder relation, an associative and commutative addition operation, a subtraction operation, ordered subtraction, and if addition of elements in `α` is covariant, then for any four elements `a`, `b`, `c`, and `d` in `α`, subtracting the sum of `c` and `d` from the sum of `a` and `b` is always less than or equal to the result of subtracting `c` from `a` and then adding the result of subtracting `d` from `b`. In LaTeX mathematics, this is expressed as:
\[a + b - (c + d) \leq a - c + (b - d)\]
More concisely: For any type `α` with a preorder, associative and commutative addition and subtraction operations, where addition is covariant, we have `a + b - (c + d) <= a - c + (b - d)` for all `a, b, c, d` in `α`.
|
tsub_add_eq_tsub_tsub
theorem tsub_add_eq_tsub_tsub :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
(a b c : α), a - (b + c) = a - b - c
This theorem states that for any set `α` of elements that is a partially ordered set, an additive commutative semigroup, and has a subtraction operation that respects the order, the subtraction of the sum `(b + c)` from `a` is equivalent to the subtraction of `c` from the result of subtracting `b` from `a`. In mathematical terms, this theorem states that `a - (b + c) = a - b - c` for all elements `a`, `b`, and `c` in `α`.
More concisely: For any additive commutative semigroup `α` with a subtraction operation respecting the order, the subtraction of `c` from `a - b` equals `a - (b + c)`.
|
AddLECancellable.add_tsub_cancel_left
theorem AddLECancellable.add_tsub_cancel_left :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b : α}, AddLECancellable a → a + b - a = b
This theorem states that for any type `α` that has a partial order, an additive commutative semigroup structure, and an ordered subtraction operation, given any two elements `a` and `b` of type `α` where `a` is 'addition-left-cancellable' (meaning that if `a + b ≤ a + c` then `b ≤ c`), we have that `a + b - a` equals `b`. Essentially, this theorem represents the property that we can add `a` to `b`, subtract `a`, and end up with `b` if and only if `a` is 'addition-left-cancellable'.
More concisely: If `α` is a type with a partial order, an additive commutative semigroup structure, and an ordered subtraction operation, and `a` is addition-left-cancellable in `α`, then `a + b - a` equals `b` for all `b` in `α`.
|
le_tsub_add
theorem le_tsub_add :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
b ≤ b - a + a
This theorem states that for any type `α` with a preorder relation (i.e., a binary relation that is reflexive and transitive), addition, and subtraction operations, and also satisfying the property of ordered subtraction, for any two elements `a` and `b` of type `α`, `b` is always less than or equal to the result of subtracting `a` from `b` and then adding `a` back. In mathematical terms, for all `a` and `b` in `α`, we have the inequality `b ≤ b - a + a`.
More concisely: For any type `α` with a preorder relation, addition, subtraction, and the property of ordered subtraction, for all `a` and `b` in `α`, we have `b ≤ a + (b - a)`.
|
tsub_le_tsub_right
theorem tsub_le_tsub_right :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b : α}, a ≤ b → ∀ (c : α), a - c ≤ b - c
This theorem states that for any type `α` which is a preorder, an additive commutative semigroup, has a subtraction operation, and supports ordered subtraction, if `a` and `b` are elements of this type such that `a` is less than or equal to `b`, then for any other element `c` of this type, `a - c` is less than or equal to `b - c`. In other words, subtracting the same quantity from two elements in an order does not change the order relation between them.
More concisely: For any preorder type `α` that is an additive commutative semigroup with subtraction and ordered subtraction, if `a ≤ b`, then `a - c ≤ b - c` for all `c` in `α`.
|
tsub_zero
theorem tsub_zero :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [inst : OrderedSub α] (a : α),
a - 0 = a
This theorem, `tsub_zero`, states that for any element `a` in a type `α`, where `α` is a partially ordered set, an additive commutative monoid, and a subtractable set with order-respecting subtraction, subtracting zero from `a` will always yield `a`. In the language of mathematics, this theorem is simply stating that `a - 0 = a` for any `a` in such a type `α`.
More concisely: For any element `a` in a type `α` that is a partially ordered set, an additive commutative monoid, and a subtractable set with order-respecting subtraction, `a - 0 = a`.
|
lt_tsub_of_add_lt_left
theorem lt_tsub_of_add_lt_left :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α} [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a + c < b → c < b - a
This theorem states that for any type `α` that has a partial order, an addition commutative semigroup structure, a subtraction operation, and an ordered subtraction operation, if `a + c` is less than `b` then `c` is less than `b - a`. This holds when there is an instance of a contravariant class in `α` which respects addition and order. The theorem suggests that this lemma may also hold for `ENNReal`, but the current proof does not work for this case. There's a thought to potentially add this lemma as a field to `OrderedSub`.
More concisely: For any type `α` with a partial order, an commutative semigroup addition, subtraction, and ordered subtraction operations, if `a + c` is less than `b`, then `c` is less than `b - a`.
|
tsub_le_iff_right
theorem tsub_le_iff_right :
∀ {α : Type u_1} [inst : LE α] [inst_1 : Add α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b c : α},
a - b ≤ c ↔ a ≤ c + b
This theorem, `tsub_le_iff_right`, states that for any type `α` with the characteristics of being orderable, subtractable, addable, and less-than-or-equal-to comparable, for any three elements of type `α` named `a`, `b`, and `c`, it holds that `a` minus `b` is less than or equal to `c` if and only if `a` is less than or equal to the sum of `c` and `b`.
More concisely: For any orderable, subtractable, addable type `α` and elements `a`, `b`, and `c` of `α`, `a - b ≤ c` if and only if `a ≤ c + b`.
|
add_tsub_le_left
theorem add_tsub_le_left :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b : α}, a + b - a ≤ b
This theorem states that for any type `α` which is a preorder, an additive commutative semigroup, and has an ordered subtraction operation, for any two elements `a` and `b` of `α`, the result of adding `a` and `b` and then subtracting `a` is less than or equal to `b`. That is, in the context of these algebraic structures, adding an element to another and then subtracting the first element does not increase the value of the second element. It corresponds to the inequality `$a + b - a \leq b$` in standard mathematical notation.
More concisely: For any preorder type `α` that is an additive commutative semigroup with an ordered subtraction operation, the law of tricommutativity holds: `a + b - a ≤ b`.
|
AddLECancellable.le_tsub_of_add_le_left
theorem AddLECancellable.le_tsub_of_add_le_left :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α}, AddLECancellable a → a + b ≤ c → b ≤ c - a
The theorem `AddLECancellable.le_tsub_of_add_le_left` states that for any type `α` that has a preorder, is an additive commutative semigroup, and has a subtract operation with ordering compatibility, if an element `a` in this type is left-erasable (i.e., `AddLECancellable a`), then for all elements `b` and `c` in `α`, if `a + b` is less than or equal to `c`, then `b` is less than or equal to `c - a`. In other words, if adding `a` to `b` doesn't exceed `c`, then `b` doesn't exceed the result of subtracting `a` from `c`.
More concisely: If `α` is a preorder, additive commutative semigroup with subtractive ordering compatibility and `a` is left-erasable in `α`, then for all `b` and `c` in `α`, if `a + b ≤ c`, then `b ≤ c - a`.
|
tsub_nonpos_of_le
theorem tsub_nonpos_of_le :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommMonoid α] [inst_2 : Sub α] [inst_3 : OrderedSub α] {a b : α},
a ≤ b → a - b ≤ 0
This theorem, `tsub_nonpos_of_le`, states that for any type `α` that has a preorder relation, an additive commutative monoid structure, a subtraction operation, and an ordered subtraction operation, if `a` and `b` are elements of `α` and `a` is less than or equal to `b`, then `a - b` is less than or equal to zero. This is an alias of the reverse direction of the `tsub_nonpos` theorem.
More concisely: For all types `α` with a preorder, additive commutative monoid structure, and ordered subtraction, if `a ≤ b`, then `a - b ≤ 0`.
|
tsub_tsub
theorem tsub_tsub :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst : OrderedSub α]
(b a c : α), b - a - c = b - (a + c)
This theorem, `tsub_tsub`, is applicable for any type `α` that satisfies the properties of a PartialOrder, an AddCommSemigroup, a Subtraction operation, and an OrderedSubtraction. The theorem states that for any three elements `b`, `a`, and `c` of type `α`, the operation of subtracting `a` and `c` from `b` separately in sequence (i.e., `(b - a) - c`) is equivalent to subtracting the sum of `a` and `c` from `b` in a single step (i.e., `b - (a + c)`). In mathematical terms, this theorem asserts the property: `b - a - c = b - (a + c)`.
More concisely: For any type `α` with PartialOrder, AddCommSemigroup, Subtraction, and OrderedSubtraction structures, the sequence of operations `(a - b) - c` and `a - (b + c)` are equal for all `a, b, c ∈ α`.
|
tsub_tsub_le
theorem tsub_tsub_le :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b : α}, b - (b - a) ≤ a
This theorem, `tsub_tsub_le`, states that for any type `α` that has a preorder (a binary relation indicating that, for every pair of elements in the set, one of the elements precedes the other), is an additive commutative semigroup (an algebraic structure consisting of a set together with an associative binary operation that has an identity element and all elements in the set are commutative under this operation), and supports subtraction and ordered subtraction, then for any two elements `a` and `b` from `α`, the result of subtracting `(b - a)` from `b` is less than or equal to `a`. In mathematical notation, this can be represented as: `b - (b - a) ≤ a`.
More concisely: For any additive commutative semigroup with subtraction and ordered subtraction, the left cancellation law holds: i.e., for all elements `a` and `b`, `b - (b - a) ≤ a`.
|
tsub_le_tsub_left
theorem tsub_le_tsub_left :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a ≤ b → ∀ (c : α), c - b ≤ c - a
This theorem, `tsub_le_tsub_left`, states that for any type `α` that has a pre-order, addition that is commutative and associative, subtraction, and ordered subtraction, and for any elements `a` and `b` of `α` such that `a` is less than or equal to `b`, the inequality `c - b ≤ c - a` holds for all `c` in `α`. In simpler terms, it says that if `a` is less than or equal to `b`, then subtracting `b` from any number `c` will always be less than or equal to subtracting `a` from `c`. This is a property of ordered groups or rings, and is often referred to as the principle of subtracting larger numbers results in smaller numbers.
More concisely: For any commutative and associative additive pre-order type `α` and elements `a ≤ b` in `α`, for all `c` in `α`, we have `c - b ≤ c - a`.
|
add_tsub_add_le_tsub_right
theorem add_tsub_add_le_tsub_right :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + c - (b + c) ≤ a - b
This theorem states that for any type `α` that has an order (`Preorder`), an addition operation (`AddCommSemigroup`), a subtraction operation (`Sub`), and an order relation compatible with subtraction (`OrderedSub`), and satisfies the `CovariantClass` property for addition and order, the inequality `a + c - (b + c) ≤ a - b` holds for any elements `a`, `b`, and `c` of this type. The proof of this theorem is not shown here. This theorem can be understood as a property of ordered groups where adding the same element `c` to `a` and `b` and then subtracting the results, is less than or equal to just subtracting `b` from `a`. For the corresponding equation, see the theorem `add_tsub_add_eq_tsub_right`.
More concisely: For any type endowed with an order, an additive commutative semigroup structure, and an order relation compatible with subtraction that satisfies the covariance property for addition and order, the inequality a + c - (b + c) ≤ a - b holds for all a, b, and c.
|
lt_of_tsub_lt_tsub_left
theorem lt_of_tsub_lt_tsub_left :
∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α]
[inst_3 : OrderedSub α] [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a - b < a - c → c < b
This theorem states that, given any linearly ordered, additive commutative semigroup with subtraction (where subtraction is an ordered operation), such that addition is a covariant operation, if the difference of 'a' and 'b' is less than the difference of 'a' and 'c', then 'c' is less than 'b'. This can be seen as a statement about the relative positions of 'a', 'b', and 'c' on the number line, where subtraction corresponds to distance.
More concisely: If 'a' is a linearly ordered, additive commutative semigroup with subtraction, and the difference of 'a' and 'b' is less than the difference of 'a' and 'c', then 'c' is less than 'b'.
|
le_tsub_of_add_le_right
theorem le_tsub_of_add_le_right :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α} [inst_4 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a + b ≤ c → a ≤ c - b
This theorem states that for any type `α` that has the properties of a Preorder (reflexivity and transitivity), an Additive Commutative Semigroup (associative and commutative addition), and Subtraction that is ordered, if `a + b` is less than or equal to `c`, then `a` is less than or equal to `c - b`. This theorem also assumes a `ContravariantClass`, which means that the addition operation (`x + x_1`) is contravariant in the sense that if by adding some elements the second argument decreases, then the result increases.
More concisely: If `α` is a preorder with reflexive and transitive relation, an additive commutative semigroup with contravariant addition, and subtraction ordered, then for all `a, b, c` in `α`, if `a + b ≤ c`, then `a ≤ c - b`.
|
add_tsub_le_tsub_add
theorem add_tsub_le_tsub_add :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α} [inst_4 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a + b - c ≤ a - c + b
This theorem, `add_tsub_le_tsub_add`, states that for any type `α` that has a preorder relation, is an additive commutative semigroup, has a subtraction operation, and is an ordered subtraction, if the addition operation is covariant (i.e., if `x + y ≤ z + w` whenever `x ≤ y` and `z ≤ w`), then for any elements `a`, `b`, and `c` of type `α`, the inequality `a + b - c ≤ a - c + b` holds. This is a property of ordered subtraction in the context of preordered additive semigroups.
More concisely: In a preordered additive semigroup with covariant addition and subtraction, the inequality `a + b - c <= a - c + b` holds for all elements `a`, `b`, and `c`.
|
tsub_le_iff_tsub_le
theorem tsub_le_iff_tsub_le :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α}, a - b ≤ c ↔ a - c ≤ b
This theorem states that for any type `α` which has an order defined (`Preorder α`), an addition operation (`AddCommSemigroup α`), a subtraction operation (`Sub α`), and a subtraction operation that respects the order (`OrderedSub α`), and for any three elements `a`, `b`, and `c` of this type, the condition "the result of subtracting `b` from `a` is less than or equal to `c`" is equivalent to "the result of subtracting `c` from `a` is less than or equal to `b`". This theorem is a formalization of a property of subtraction in the context of pre-ordered commutative additive groups.
More concisely: For any pre-ordered commutative additive group `(α, <, +)`, for all `a, b, c ∈ α`, `a - b ≤ c` if and only if `c - a ≤ b`.
|
le_add_tsub
theorem le_add_tsub :
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b : α}, a ≤ b + (a - b)
This theorem, `le_add_tsub`, states that for any type `α` that satisfies the conditions of being a preorder, an additive commutative semigroup, and an ordered subtraction operation, for any two elements `a` and `b` of `α`, `a` is less than or equal to the result of adding `b` to the difference of `a` and `b`. In mathematical terms, for all `a` and `b` in `α`, we have `a ≤ b + (a - b)`.
More concisely: For all `α` with preorder, additive commutative semigroup structure, and ordered subtraction, and all `a` and `b` in `α`, we have `a ≤ b + (a - b)`.
|
lt_tsub_iff_right
theorem lt_tsub_iff_right :
∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α]
[inst_3 : OrderedSub α], a < b - c ↔ a + c < b
The theorem `lt_tsub_iff_right` states that for any type `α`, and any three elements `a`, `b`, and `c` of type `α` (where `α` is a linear ordered additive commutative semigroup with an ordered subtraction operation), the inequality `a` is less than the difference `b - c` is equivalent to the inequality `a + c` is less than `b`. It essentially shows a relationship between subtraction and addition in an ordered mathematical structure.
More concisely: For any linear ordered additive commutative semigroup type `α` and elements `a, b, c` of `α`, `a < b - c` if and only if `a + c < b`.
|
AddLECancellable.lt_tsub_of_add_lt_right
theorem AddLECancellable.lt_tsub_of_add_lt_right :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α}, AddLECancellable c → a + c < b → a < b - c
The theorem `AddLECancellable.lt_tsub_of_add_lt_right` states that for any partially ordered commutative semigroup `α` with subtraction that preserves order, and for any elements `a`, `b`, and `c` of `α`, if `c` is left order-reflecting with respect to addition (i.e., `c` is `AddLECancellable`), and if `a + c` is less than `b`, then `a` is less than `b - c`. In other words, if adding `c` to `a` results in a value less than `b`, and if `c` has the property that adding it to any two elements preserves their order, then `a` is less than the difference of `b` and `c`.
More concisely: If `α` is a commutative semigroup with subtraction preserving order, `c` is `AddLECancellable` in `α`, and `a + c < b`, then `a < b - c`.
|
AddLECancellable.lt_tsub_of_add_lt_left
theorem AddLECancellable.lt_tsub_of_add_lt_left :
∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
{a b c : α}, AddLECancellable a → a + c < b → c < b - a
The theorem `AddLECancellable.lt_tsub_of_add_lt_left` states that for any type `α` that has a partial order, a commutative semigroup structure under addition, a subtraction operation, and an ordered subtraction operation, if an element `a` of `α` is left-cancellable under addition (i.e., whenever adding `a` to two other elements `b` and `c` results in `b` being less than or equal to `c`, then `b` itself is less than or equal to `c`, as per the definition of `AddLECancellable`), then for any elements `b` and `c` of `α`, if the sum of `a` and `c` is less than `b`, then `c` is less than the difference of `b` and `a`. In terms of mathematical notation, this can be written as: if $a$ is AddLECancellable and $a + c < b$, then $c < b - a$.
More concisely: If `α` is a type with a partial order, commutative semigroup structure under addition, subtraction, and ordered subtraction, and `a` is left-cancellable in `α`, then for all `b` and `c`, if `a + c < b`, then `c < b - a`.
|
lt_of_tsub_lt_tsub_right
theorem lt_of_tsub_lt_tsub_right :
∀ {α : Type u_1} {a b c : α} [inst : LinearOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α]
[inst_3 : OrderedSub α], a - c < b - c → a < b
This theorem, `lt_of_tsub_lt_tsub_right`, states that for any type `α` that has a linear order, an additive commutative semigroup structure, a subtraction operation, and an ordered subtraction, if the difference between `a` and `c` is less than the difference between `b` and `c`, then `a` is less than `b`. In other words, for all `a`, `b`, and `c` of such a type `α`, if `a - c < b - c`, then `a < b`. This is essentially a translation of the property of "subtracting the same amount from two numbers preserves the order" into the language of type theory.
More concisely: If `α` is a type with a linear order, an additive commutative semigroup structure, a subtraction operation, and an ordered subtraction, then for all `a`, `b`, and `c` of type `α`, if `a - c < b - c`, then `a < b`.
|