tsub_eq_zero_of_le
theorem tsub_eq_zero_of_le :
∀ {α : Type u_1} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
a ≤ b → a - b = 0
This theorem, `tsub_eq_zero_of_le`, states that for any type `α` which is a canonically ordered additive commutative monoid where subtraction is defined and order-preserving, if `a` and `b` are any two elements of `α` and `a` is less than or equal to `b`, then the result of `a` subtract `b` will be zero. This is essentially a formalization of the principle that in an ordered set, subtracting a larger number from a smaller one (or the same number from itself) yields zero.
More concisely: For any additively commutative, order-preserving, and canonically ordered monoid type `α`, if `a ≤ b` then `a - b = 0`.
|
AddLECancellable.tsub_tsub_cancel_of_le
theorem AddLECancellable.tsub_tsub_cancel_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b : α}, AddLECancellable (b - a) → a ≤ b → b - (b - a) = a
The theorem `AddLECancellable.tsub_tsub_cancel_of_le` states that for any type `α` that is equipped with an addition operation making it an additive commutative semigroup, a partial order `≤`, additive associativity, subtraction operation, and an ordered subtraction, if an element `b - a` of this type is 'add-Le-cancellable' (meaning order is preserved when an element is added), and if `a` is less than or equal to `b`, then the result of subtracting `(b - a)` from `b` is `a`. In simpler terms, if we assume that adding to `b - a` keeps the order, and `a` is not greater than `b`, then taking away `b - a` from `b` gives us `a`, which is a form of the subtraction cancellation law.
More concisely: If `α` is an additive commutative semigroup with partial order `≤`, additive associativity, subtraction, and ordered subtraction, and if `a ≤ b` and `b - a` is add-Le-cancellable, then `b - (b - a) = a`.
|
add_tsub_cancel_iff_le
theorem add_tsub_cancel_iff_le :
∀ {α : Type u_1} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
a + (b - a) = b ↔ a ≤ b
This theorem, `add_tsub_cancel_iff_le`, states that for any canonically ordered additive commutative monoid `α` that also supports subtraction and ordered subtraction, given any two elements `a` and `b` of `α`, the equality `a + (b - a) = b` holds if and only if `a` is less than or equal to `b`. In simpler terms, adding `a` to the difference of `b` and `a` yields `b` if and only if `a` is not greater than `b`.
More concisely: For any additive commutative monoid with subtraction and order relation, element `a` is less than or equal to `b` if and only if `a + (b - a) = b`.
|
tsub_eq_iff_eq_add_of_le
theorem tsub_eq_iff_eq_add_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
b ≤ a → (a - b = c ↔ a = c + b)
This theorem states that for any type `α` which forms an additive commutative semigroup, has a partial order, has an addition operation that obeys the order, has a subtraction operation, and the subtraction is ordered, given three elements `a`, `b`, and `c` of type `α`, if `b` is less than or equal to `a`, then `a - b` equals `c` if and only if `a` is equal to `c + b`. This essentially expresses how subtraction can be seen as the addition of the negation.
More concisely: For any additive commutative semigroup `α` with a partial order and ordered subtraction, if `b ≤ a` then `a = c + b` if and only if `a = c + b` and `b = a - c`.
|
tsub_add_cancel_of_le
theorem tsub_add_cancel_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b : α}, a ≤ b → b - a + a = b
This theorem states that for any type `α` that has the structure of an additive commutative semigroup, a partial order, a structure that allows for the existence of an additive operation given a less-than-or-equal-to relation, a covariant class with respect to the plus operation and less-than-or-equal-to relation, and ordered subtraction operation, if `a` is less than or equal to `b`, then subtracting `a` from `b` and adding `a` results in `b`. In simpler terms, it's proving the cancellation property: if you subtract a number from another and then add it back, you get the original number.
More concisely: For any additive commutative semigroup `α` with a partial order and covariant subtraction, if `a ≤ b`, then `b = a + (b - a)`.
|
tsub_tsub_eq_add_tsub_of_le
theorem tsub_tsub_eq_add_tsub_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α HAdd.hAdd LE.le], c ≤ b → a - (b - c) = a + c - b
The theorem `tsub_tsub_eq_add_tsub_of_le` states that for any type `α` that has an addition operation forming a commutative semigroup, a partial order relation, a subtraction operation, an `ExistsAddOfLE` instance (meaning that for any two elements `x` and `y` in `α`, if `x ≤ y`, then there exists a `z` such that `x + z = y`), a `CovariantClass` instance (meaning that adding an element to the right preserves the order), and a `ContravariantClass` instance (meaning that adding an element to the left reverses the order), if we have three elements `a`, `b`, and `c` from `α` such that `c` is less than or equal to `b`, then the difference of `a` and the difference of `b` and `c` equals the difference of the sum of `a` and `c`, and `b`. In standard mathematical notation, this can be represented as `a - (b - c) = a + c - b` whenever `c ≤ b`.
More concisely: For any commutative semigroup `α` with a partial order relation, subtraction, `ExistsAddOfLE`, `CovariantClass`, and `ContravariantClass` instances, if `c ≤ b`, then `a - (b - c) = a + c - b`.
|
add_tsub_assoc_of_le
theorem add_tsub_assoc_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
c ≤ b → ∀ (a : α), a + b - c = a + (b - c)
The theorem `add_tsub_assoc_of_le` states that for any type `α` that is an additive commutative semigroup, has a partial order, an existence of addition for elements less than or equal to each other, a variant class, a subtraction operation, an ordered subtraction, and a contravariant class, if `c` is less than or equal to `b`, then for any `a` in `α`, the operation `a + b - c` is equal to `a + (b - c)`. This theorem provides a property of associative operations involving addition and subtraction under certain conditions in an ordered additive structure.
More concisely: For any additive commutative semigroup `α` with partial order, existence of addition for elements less than or equal to each other, variant and contravariant classes, if `c ≤ b`, then `a + (b - c) = a + b - c` for all `a` in `α`.
|
lt_of_tsub_lt_tsub_right_of_le
theorem lt_of_tsub_lt_tsub_right_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst : OrderedSub α]
{a b c : α}, c ≤ b → a - c < b - c → a < b
This theorem states that for any type `α` which is an additive commutative semigroup, has a partial order, has an addition operation for less than or equal to comparisons, has a covariant class for addition and comparison, and has a subtraction operation with an ordered subtraction property, if we have three elements `a`, `b`, and `c` such that `c` is less than or equal to `b` and `a - c` is less than `b - c`, then `a` is less than `b`. Note that there is a stronger statement in a linear order, as referred to in `lt_of_tsub_lt_tsub_right`.
More concisely: If `α` is an additive commutative semigroup with partial order, covariant additive class, and ordered subtraction property, and `a`, `b`, `c` are elements of `α` with `c ≤ b` and `a - c < b - c`, then `a < b`.
|
tsub_lt_tsub_iff_left_of_le_of_le
theorem tsub_lt_tsub_iff_left_of_le_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (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],
b ≤ a → c ≤ a → (a - b < a - c ↔ c < b)
This theorem states that for any type `α` that is an additive commutative semigroup, has a partial order, has an operation "add of less than or equal", exhibits covariance and contravariance, and supports subtraction and ordered subtraction, if two elements `b` and `c` are both less than or equal to another element `a`, then the statement "the difference of `a` and `b` is less than the difference of `a` and `c`" is equivalent to the statement "c is less than b". This is a specific case of a related theorem for linear orders.
More concisely: For any additive commutative semigroup with a partial order, covariance, contravariance, subtraction, and ordered subtraction, if `b ≤ a` and `c ≤ a`, then `a - b ≤ a - c` if and only if `c ≤ b`.
|
tsub_lt_iff_right
theorem tsub_lt_iff_right :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
b ≤ a → (a - b < c ↔ a < c + b)
This theorem, `tsub_lt_iff_right`, holds for any type `α` that is an additive commutative semigroup, has a partial order, has an operation for the existence of addition of less than or equal to, exhibits covariance and contravariance with respect to addition and less than or equal, and supports subtraction operations where addition and subtraction are ordered. The theorem states that for any three elements `a`, `b`, `c` of type `α`, if `b` is less than or equal to `a`, then the inequality `a - b < c` holds true if and only if `a < c + b`. This theorem essentially establishes an equivalence between two different ways of expressing similar inequalities.
More concisely: For any additive commutative semigroup type `α` with partial order, additive subtraction, and covariance/contravariance properties, the inequality `a - b < c` is equivalent to `a < c + b`.
|
tsub_self
theorem tsub_self :
∀ {α : Type u_1} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] (a : α),
a - a = 0
This theorem, `tsub_self`, states that for any type `α` that forms a canonically ordered additive commutative monoid, and where this type `α` supports subtraction and ordered subtraction operations, subtracting any value `a` of type `α` from itself will always result in zero. Essentially, this theorem is the formal representation in Lean 4 of the familiar arithmetic property that a number minus itself equals zero.
More concisely: For any type `α` that is a commutative monoid with additive and ordered subtraction operations, `a - a = 0` for all `a` of type `α`.
|
le_tsub_iff_right
theorem le_tsub_iff_right :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a ≤ c → (b ≤ c - a ↔ b + a ≤ c)
The theorem `le_tsub_iff_right` states that for any type `α` that has an addition and subtraction operation, and is also a partially ordered commutative semigroup, if `a` is less than or equal to `c`, then `b` is less than or equal to `c - a` if and only if `b + a` is less than or equal to `c`. This theorem essentially describes a property of subtraction in the context of ordered algebraic structures.
More concisely: For any commutative semigroup with addition and order structure, if `a ≤ c` and `b ≤ a`, then `b ≤ c - a` if and only if `b + a ≤ c`.
|
tsub_le_self
theorem tsub_le_self :
∀ {α : Type u_1} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
a - b ≤ a
This theorem states that for any type `α` that is a canonically ordered additive commutative monoid (where addition is associative, commutative, and has an identity element, and there exists a canonical total order compatible with the addition), which also supports subtraction and the subtraction operation is ordered, the result of subtracting any element `b` from another element `a` is always less than or equal to `a`. In other words, for all `a` and `b` in `α`, `a - b ≤ a`.
More concisely: For any canonically ordered, additive commutative monoid `α` with subtraction that respects the order, for all `a` and `b` in `α`, `a - b ≤ a`.
|
le_tsub_iff_left
theorem le_tsub_iff_left :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a ≤ c → (b ≤ c - a ↔ a + b ≤ c)
This theorem, `le_tsub_iff_left`, states that for any type `α` that has the structure of an additive commutative semigroup, a partial order, satisfies the existence of addition from less than or equal to (`ExistsAddOfLE`), is a covariant class and contravariant class under a certain condition, and has subtraction operation and an ordered subtraction, if `a` is less than or equal to `c` then the statement `b` is less than or equal to `c - a` is equivalent to the statement `a + b` is less than or equal to `c`.
More concisely: For any additive commutative semigroup with a partial order, existence of addition from less than or equal to, and ordered subtraction, if `a ≤ c` then `b ≤ c - a` if and only if `a + b ≤ c`.
|
tsub_tsub_assoc
theorem tsub_tsub_assoc :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
b ≤ a → c ≤ b → a - (b - c) = a - b + c
This theorem, `tsub_tsub_assoc`, states that for any type `α` that forms an additive commutative semigroup, has a partial order, has an operation of addition that exists for less than or equal to, is a covariant and contravariant class with respect to addition and less than or equal to, and has subtraction operation that is ordered, then for any three elements `a`, `b`, and `c` in `α`, if `b` is less than or equal to `a` and `c` is less than or equal to `b`, the result of calculating `a - (b - c)` is equal to `a - b + c`. This theorem describes the associative property of subtraction in the context of an ordered additive commutative semigroup.
More concisely: In an additive commutative semigroup with subtraction operation that respects the order, the subtraction is associative: `a - (b - c) = a - b + c`, given `a >= b >= c`.
|
tsub_lt_iff_left
theorem tsub_lt_iff_left :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
b ≤ a → (a - b < c ↔ a < b + c)
This theorem states that for any type `α` that has the structure of an additive commutative semigroup, a partial order, an addition operation for elements that satisfy the less than or equals relation, a subtract operation, and an ordered subtract operation, and also satisfies the covariant and contravariant properties, if `b` is less than or equal to `a`, then `a - b` is less than `c` if and only if `a` is less than `b + c`.
More concisely: For any additive commutative semigroup `α` with a partial order and ordered subtraction satisfying covariant and contravariant properties, if `a ≤ b` and `b + c`, then `a ≤ c + b`.
|
add_tsub_cancel_of_le
theorem add_tsub_cancel_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b : α}, a ≤ b → a + (b - a) = b
This theorem, `add_tsub_cancel_of_le`, states that for any type `α` that has the structure of an additive commutative semigroup, a partial order, and an existence of addition for elements less than or equal to another, and also has the properties of being a subclass and having subtraction with a specific order, given two elements `a` and `b` of that type where `a` is less than or equal to `b`, the sum of `a` and the difference of `b` and `a` is equal to `b`. This theorem is essentially the algebraic property that adding the difference of two numbers to the smaller number yields the larger number, formalized in the context of ordered semigroups.
More concisely: For any additive commutative semigroup with order and subtraction, if `a` is less than or equal to `b`, then `a + (b - a) = b`.
|
AddLECancellable.tsub_lt_iff_left
theorem AddLECancellable.tsub_lt_iff_left :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α}, AddLECancellable b → b ≤ a → (a - b < c ↔ a < b + c)
The theorem `AddLECancellable.tsub_lt_iff_left` applies to an additive commutative semi-group that is also a partially ordered set on which subtraction is defined in a specific way. Given elements `a`, `b`, and `c` of this set, if `b` is add-left-cancellable and `b` is less than or equal to `a`, then the theorem states that `a` minus `b` is less than `c` if and only if `a` is less than `b + c`. Here, `b` is said to be add-left-cancellable if for any two elements `x` and `y` of the set, `b + x` being less than or equal to `b + y` implies `x` is less than or equal to `y`.
More concisely: Given an additive commutative semi-group with subtraction that is also a partially ordered set, if `b` is add-left-cancellable and `b <= a`, then `a - b < c` if and only if `a < b + c`.
|
lt_tsub_iff_right_of_le
theorem lt_tsub_iff_right_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
c ≤ b → (a < b - c ↔ a + c < b)
The theorem `lt_tsub_iff_right_of_le` establishes an equivalence relation about subtraction and comparison in the context of a partially ordered additive commutative semigroup with certain properties. Specifically, given types `α` with instances of `AddCommSemigroup`, `PartialOrder`, `ExistsAddOfLE`, `CovariantClass`, `Sub`, `OrderedSub`, and `ContravariantClass`, and three elements `a`, `b`, `c` of type `α`, the theorem states that if `c` is less than or equal to `b`, then `a` is less than `b - c` if and only if `a + c` is less than `b`.
More concisely: For all additively commutative semigroups `α` with partial order and the given properties, if `c ≤ b` then `a < b - c` if and only if `a + c < b`.
|
AddLECancellable.le_tsub_iff_left
theorem AddLECancellable.le_tsub_iff_left :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α}, AddLECancellable a → a ≤ c → (b ≤ c - a ↔ a + b ≤ c)
The theorem `AddLECancellable.le_tsub_iff_left` states that for any type `α` that has an addition operation forming a commutative semigroup, a partial order, an existence of an addition operation that respects this order, a subtraction operation, and an ordered subtraction operation, and for any elements `a`, `b`, and `c` of this type, if `a` is `AddLECancellable` (which means that addition with `a` is order-reflecting) and `a` is less than or equal to `c`, 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 essentially relates the order of elements in this type with their sum and difference, under the premise that addition with a certain element reflects the order.
More concisely: For any commutative semigroup with addition, partial order, order-reflecting additive element `a`, and ordered subtraction, if `a` is less than or equal to `c` and `a` is AddLECancellable, then `b` is less than or equal to `c - a` if and only if `a + b` is less than or equal to `c`.
|
tsub_add_tsub_cancel
theorem tsub_add_tsub_cancel :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α}, b ≤ a → c ≤ b → a - b + (b - c) = a - c
This theorem, `tsub_add_tsub_cancel`, states that for any type `α` that has an additive commutative semigroup structure, a partial order, the ability to find an additive element satisfying a less than or equal to relation, follows covariant laws with respect to addition and order, and also supports subtraction operation that respects the order, the following holds: for any three elements `a`, `b`, and `c` of `α` such that `b` is less than or equal to `a` and `c` is less than or equal to `b`, the expression `a - b + (b - c)` is equal to `a - c`. This is a generalized property related to order and arithmetic operations, particularly subtraction and addition, in this mathematical structure.
More concisely: For any additive commutative semigroup with order relation and subtraction operation, if `a` is greater than or equal to `b` and `b` is greater than or equal to `c`, then `a - b + (b - c) = a - c`.
|
tsub_add_eq_add_tsub
theorem tsub_add_eq_add_tsub :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
b ≤ a → a - b + c = a + c - b
This theorem states that for any type `α` that has the structures of an additive commutative semigroup, a partial order, and an ordered subtraction, and also satisfies certain properties related to addition and less-than-or-equal (`≤`) operation, if `b` is less than or equal to `a`, then subtracting `b` from `a` and then adding `c` (`a - b + c`) is equal to first adding `c` to `a` and then subtracting `b` (`a + c - b`).
More concisely: For all additive commutative semigroups `α` with partial order and ordered subtraction where `a ≤ b` implies `(a + c) - b = a - b + c`, for all `a, b, c` in `α`.
|
tsub_pos_of_lt
theorem tsub_pos_of_lt :
∀ {α : Type u_1} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
a < b → 0 < b - a
This theorem, `tsub_pos_of_lt`, states that for any type `α` that is a canonically ordered additive commutative monoid and also supports subtraction and ordered subtraction, if `a` and `b` are elements of `α` and `a` is less than `b`, then the result of `b - a` is greater than zero. Essentially, in a context where subtraction is well-behaved and the elements are ordered in a sensible way, subtracting a smaller number from a larger one produces a positive result.
More concisely: If `α` is a canonically ordered additive commutative monoid with subtraction and ordered subtraction, then for all `a` and `b` in `α` with `a` less than `b`, `b - a` is positive.
|
eq_tsub_iff_add_eq_of_le
theorem eq_tsub_iff_add_eq_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
c ≤ b → (a = b - c ↔ a + c = b)
This theorem is about certain properties of an ordered and additive set. For any given type `α`, that forms an additive commutative semigroup, a partial order, and for which addition operation is monotonic and subtraction operation is defined and respects order, if an instance `c` is less than or equal to an instance `b`, then `a` is equal to the difference `b - c` if and only if `a + c` is equal to `b`. In terms of arithmetic, it states that in a setting where all the relevant operations and orderings are defined and behave properly, subtracting a value from another and adding that value back gives you the original number.
More concisely: For any additive commutative semigroup `α` with monotonic addition and defined subtraction respecting order, if `c ≤ b` then `a = b - c` if and only if `a + c = b`.
|
tsub_pos_iff_lt
theorem tsub_pos_iff_lt :
∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
{a b : α}, 0 < a - b ↔ b < a
This theorem states that for any type `α`, which is a canonically linearly ordered additive commutative monoid with a subtraction operation and an order relation compatible with subtraction, the difference `a - b` is positive if and only if `b` is less than `a`. In other words, the theorem provides a relationship between the positivity of the subtraction of two elements and the order of these two elements in the context of a specific algebraic structure.
More concisely: For any canonically linearly ordered additive commutative monoid type `α` with subtraction operation and compatible order relation, `a - b` is positive if and only if `b` is less than `a`.
|
tsub_eq_zero_iff_le
theorem tsub_eq_zero_iff_le :
∀ {α : Type u_1} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
a - b = 0 ↔ a ≤ b
This theorem, `tsub_eq_zero_iff_le`, states that for any type `α` that has an instance of a canonically ordered additive commutative monoid, an instance of subtraction, and an instance of ordered subtraction, the subtraction of two elements `a` and `b` of type `α` results in zero if and only if `a` is less than or equal to `b`. This means that in the given structures, the only way subtraction can yield zero is when the subtrahend is less than or equal to the minuend.
More concisely: For any type `α` with a canonically ordered additive commutative monoid, subtraction, and ordered subtraction, `a - b = 0` if and only if `a <= b`.
|
tsub_tsub_cancel_of_le
theorem tsub_tsub_cancel_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b : α} [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≤ b → b - (b - a) = a
This theorem, `tsub_tsub_cancel_of_le`, states that for any type `α` that is an additive commutative semigroup, has a partial order, satisfies the existence of addition of less-than-or-equal-to relations, upholds covariance and contravariance, and supports subtraction with an order, if `a` and `b` are elements of `α` and `a` is less than or equal to `b`, then subtracting the difference of `b` and `a` from `b` equals `a`. In mathematical terms, if `a ≤ b` for some `a, b` in `α`, then `b - (b - a) = a`.
More concisely: For any additive commutative semigroup `α` with a partial order, the subtraction of the difference of two elements `a` and `b` with `a ≤ b` is equal to `a`.
|
tsub_add_cancel_iff_le
theorem tsub_add_cancel_iff_le :
∀ {α : Type u_1} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
b - a + a = b ↔ a ≤ b
This theorem, `tsub_add_cancel_iff_le`, states that for all types `α` that are canonically ordered additive commutative monoids with a subtraction operation that respects the order, for any two elements `a` and `b` of type `α`, the equation `b - a + a = b` holds if and only if `a` is less than or equal to `b`. In less formal terms, this is saying that if we subtract `a` from `b` and then add `a` back, we will get `b` back if and only if `a` is not greater than `b`. This theorem is a formalized version of a familiar fact from ordinary arithmetic.
More concisely: For any additively commutative monoid with subtraction respecting the order, the subtraction and addition commute if and only if the subtrahend is less than or equal to the minuend.
|
add_le_of_le_tsub_right_of_le
theorem add_le_of_le_tsub_right_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α}, b ≤ c → a ≤ c - b → a + b ≤ c
This theorem states that for any type `α` that is an additive commutative semigroup, a partially ordered set, has an addition operation for elements satisfying less than or equal relation, and supports subtraction operation that respects the order, if an element `b` is less than or equal to another element `c`, and an element `a` is less than or equal to the difference of `c` and `b`, then the sum of `a` and `b` is less than or equal to `c`.
More concisely: If `α` is an additive commutative semigroup, a partially ordered set with respect to `≤`, and for all `a ≤ b ≤ c`, we have `a + b ≤ c`, then `α` satisfies the subadditivity property with respect to `≤`.
|
zero_tsub
theorem zero_tsub :
∀ {α : Type u_1} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] (a : α),
0 - a = 0
This theorem, named `zero_tsub`, states that for any type `α` that has a structure of a canonically ordered additive commutative monoid and also supports subtraction operation which obeys the ordering, the result of subtracting any element `a` of that type from zero is always zero. In other words, in such a structured type, zero minus any element equals zero.
More concisely: For any additively commutative monoid with subtraction operation respecting its ordering, subtracting any element from zero yields zero.
|
AddLECancellable.tsub_le_tsub_iff_left
theorem AddLECancellable.tsub_le_tsub_iff_left :
∀ {α : Type u_1} [inst : CanonicallyOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b c : α},
AddLECancellable a → AddLECancellable c → c ≤ a → (a - b ≤ a - c ↔ c ≤ b)
The theorem `AddLECancellable.tsub_le_tsub_iff_left` states that for any elements `a`, `b`, and `c` in a canonically ordered additive commutative monoid that also supports subtraction and ordered subtraction, if `a` and `c` are additive left cancellable and `c` is less than or equal to `a`, then `a - b` is less than or equal to `a - c` if and only if `c` is less than or equal to `b`. In simpler terms, it states that in such a structure, if adding a certain element to the left side of two different elements preserves the order relation, then the order relation between the differences of these elements and another element is equivalent to the order relation between the subtracted elements.
More concisely: If `a`, `b`, and `c` are elements in a canonically ordered additive commutative monoid with subtraction and ordered subtraction, then `a - b <= a - c` if and only if `c <= b`.
|
tsub_lt_self
theorem tsub_lt_self :
∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α}
[inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], 0 < a → 0 < b → a - b < a
The theorem `tsub_lt_self` states that for any type `α` that is a canonically linearly ordered additive commutative monoid with subtraction and an ordered subtraction operation, given two elements `a` and `b` of type `α` (where `a`, `b` are positive), the difference `a - b` is less than `a`. This is under the condition that `α` is a contravariant class with respect to the addition and less-than-or-equal-to operations. Essentially, this theorem is saying that subtracting a positive value from a number results in a smaller number.
More concisely: For any additively commutative, canonically linearly ordered monoid `α` with subtraction and the contravariant property with respect to addition and order, given `a`, `b` in `α` with `a > b > 0`, we have `a - b < a`.
|
lt_tsub_iff_left_of_le
theorem lt_tsub_iff_left_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
c ≤ b → (a < b - c ↔ c + a < b)
This theorem, `lt_tsub_iff_left_of_le`, states that for any type `α` that is an `AddCommSemigroup`, `PartialOrder`, `ExistsAddOfLE`, `CovariantClass`, has a subtraction operation, an `OrderedSub`, and a `ContravariantClass`, and for any three elements `a`, `b`, and `c` of type `α`, if `c` is less than or equal to `b`, then `a` is less than the difference of `b` and `c` if and only if the sum of `c` and `a` is less than `b`.
More concisely: For any `AddCommSemigroup` type `α` with order `≤`, `OrderedSub`, `ContravariantClass`, and subtraction operation, `a ≤ b` implies `a ≤ b - c` if and only if `a + c <= b`.
|
AddLECancellable.tsub_lt_tsub_iff_left_of_le
theorem AddLECancellable.tsub_lt_tsub_iff_left_of_le :
∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
{a b c : α}, AddLECancellable a → AddLECancellable b → b ≤ a → (a - b < a - c ↔ c < b)
This theorem, `AddLECancellable.tsub_lt_tsub_iff_left_of_le`, describes a property of subtraction in the context of an ordered additive commutative monoid with a canonical linear order. It states that for any three elements `a`, `b`, `c` in such a monoid, if `a` and `b` both have the property that adding them to any other element is order-reflecting (i.e., they are `AddLECancellable`), and `b` is less than or equal to `a`, then `a` minus `b` is less than `a` minus `c` if and only if `c` is less than `b`. In mathematical notation, given the conditions $a, b \in \text{AddLECancellable}(\alpha)$ and $b \leq a$, we have $(a - b) < (a - c)$ if and only if $c < b$.
More concisely: For any elements `a`, `b`, `c` in an additive commutative monoid with a canonical linear order and having the property that `a` and `b` are order-reflecting (AddLECancellable), if `b` is less than or equal to `a`, then `a - b` is less than `a - c` if and only if `c` is less than `b`.
|
tsub_lt_tsub_iff_left_of_le
theorem tsub_lt_tsub_iff_left_of_le :
∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
{a b c : α} [inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
b ≤ a → (a - b < a - c ↔ c < b)
This theorem, `tsub_lt_tsub_iff_left_of_le`, is about subtraction in a particular type of algebraic structure, canonically linearly ordered additive commutative monoids with a subtraction operation that is ordered. Given elements `a`, `b`, and `c` of such a structure, if `b` is less than or equal to `a`, then `a - b` is less than `a - c` if and only if `c` is less than `b`. This theorem provides a way to compare the results of subtraction operations in this type of structure.
More concisely: For all additively commutative, ordered monoids with subtraction `M`, and all elements `a`, `b`, and `c` in `M` with `b ≤ a`, if `a - b < a - c`, then `b < c`.
|
tsub_lt_tsub_iff_right
theorem tsub_lt_tsub_iff_right :
∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
{a b c : α} [inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
c ≤ a → (a - c < b - c ↔ a < b)
This theorem states a property about subtraction in a certain kind of mathematical structure called "canonically linear ordered additive commutative monoid" with an "ordered subtraction" operation. In this setting, for any three elements `a`, `b`, and `c`, if `c` is less than or equal to `a`, then `a` minus `c` is less than `b` minus `c` if and only if `a` is less than `b`. This essentially describes how subtracting the same amount from two quantities preserves the order between the quantities. Note that this theorem is also valid for extended non-negative real numbers, but its proof in that case is different.
More concisely: In a canonically linear ordered additive commutative monoid, for all elements `a`, `b`, and `c`, if `c` ≤ `a`, then `a - c` < `b - c` if and only if `a` < `b`.
|
AddLECancellable.le_tsub_iff_right
theorem AddLECancellable.le_tsub_iff_right :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α}, AddLECancellable a → a ≤ c → (b ≤ c - a ↔ b + a ≤ c)
The theorem `AddLECancellable.le_tsub_iff_right` states that for any type `α` that is an additive commutative semigroup and has partial order, the existence of addition of lesser elements, covariance, subtraction, and ordered subtraction, for any elements `a`, `b`, and `c` of this type, if `a` is "left-addition less-than-or-equal-to" cancellable and `a` is less than or equal to `c`, then `b` is less than or equal to `c - a` if and only if `b + a` is less than or equal to `c`.
In other words, given a certain structure of the type, and given that adding `a` to some element doesn't affect the ordering of elements, we can safely "move" `a` between sides of an inequality involving addition and subtraction.
More concisely: For any additive commutative semigroup with partial order `α`, if `a` is left- cancellable and `a ≤ c`, then `b ≤ c - a` if and only if `b + a ≤ c`.
|
AddLECancellable.tsub_lt_iff_right
theorem AddLECancellable.tsub_lt_iff_right :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α}, AddLECancellable b → b ≤ a → (a - b < c ↔ a < c + b)
This theorem states that for any type `α` that has an additive commutative semigroup structure, a partial order, a subtraction operation, and satisfies some additional properties, and any elements `a`, `b`, and `c` of `α`, if `b` is `AddLECancellable` (meaning adding `b` to any element is an order-reflecting operation) and `b` is less than or equal to `a`, then `a - b` is less than `c` if and only if `a` is less than `c + b`.
More concisely: For any additive commutative semigroup `α` with a partial order, subtraction operation, and `AddLECancellable` elements `b`, if `b` is less than or equal to `a` then `a - b` is less than `c` if and only if `a` is less than `c + b`.
|
AddLECancellable.add_tsub_assoc_of_le
theorem AddLECancellable.add_tsub_assoc_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{b c : α}, AddLECancellable c → c ≤ b → ∀ (a : α), a + b - c = a + (b - c)
The theorem `AddLECancellable.add_tsub_assoc_of_le` states that for any type `α` which is an additive commutative semigroup, has a partial order, has an existing additive counterpart of less than or equal to, exhibits covariance with respect to addition and less than or equal to relation, and has subtraction and an ordered subtraction operation, if an element `c` in `α` is less than or equal to `b` and `c` is left-cancellable with respect to addition and order (meaning that addition of `c` on the left side preserves the order of elements), then for any element `a` in `α`, the expression `a + b - c` is equal to `a + (b - c)`. In other words, adding `b` to `a`, subtracting `c`, is the same as adding `a` to the result of `b - c`.
More concisely: If `α` is an additive commutative semigroup with partial order, has an additive `≤`, exhibits covariance, and has subtraction and ordered subtraction, and `c ≤ b` and `c` is left-cancellative with respect to addition and `≤`, then `a + b - c = a + (b - c)` for all `a` in `α`.
|
lt_of_tsub_lt_tsub_left_of_le
theorem lt_of_tsub_lt_tsub_left_of_le :
∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [inst_2 : ExistsAddOfLE α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_4 : Sub α] [inst_5 : OrderedSub α]
{a b c : α} [inst_6 : ContravariantClass α α (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], c ≤ a → a - b < a - c → c < b
This theorem states that for any type `α` that is an additive commutative semigroup, has a partial order, an additive form of the less than or equal to relation, and subtraction operation, if `c` is less than or equal to `a` and `a - b` is less than `a - c`, then `c` is less than `b`. Note that the type `α` also possesses some additional properties reflected by the `CovariantClass`, `OrderedSub`, and `ContravariantClass` typeclasses.
More concisely: If `α` is an additive commutative semigroup with a partial order, an additive subtraction operation, and the relation `≤` such that `c ≤ a` and `a - b < a - c` imply `c < b`, then `α` has the property of being an ordered abelian group. (This theorem is known as the "preorder and triangle inequality for subtraction" theorem for ordered groups.)
|
AddLECancellable.tsub_lt_self
theorem AddLECancellable.tsub_lt_self :
∀ {α : Type u_1} [inst : CanonicallyLinearOrderedAddCommMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
{a b : α}, AddLECancellable a → 0 < a → 0 < b → a - b < a
The theorem `AddLECancellable.tsub_lt_self` states that, for any type `α` that is a canonically linearly ordered additive commutative monoid and also has a subtraction operation which is ordered, if an element `a` of this type is "addition-left-`≤`-cancellable" (meaning that if `a + b ≤ a + c` then it must be the case that `b ≤ c`), and if `a` and `b` are both positive (greater than `0`), then the subtraction `a - b` is strictly less than `a`. In a more mathematical language, given an element `a` such that `a + b ≤ a + c` implies `b ≤ c`, and two positive elements `a` and `b`, then `a - b < a`.
More concisely: If `α` is a canonically linearly ordered additive commutative monoid with ordered subtraction, `a` and `b` are positive elements, and `a + b ≤ a + c` implies `b leq c`, then `a - b < a`.
|