WithTop.add_right_cancel_iff
theorem WithTop.add_right_cancel_iff :
∀ {α : Type u} [inst : Add α] {a b c : WithTop α} [inst_1 : IsRightCancelAdd α], a ≠ ⊤ → (b + a = c + a ↔ b = c)
This theorem, `WithTop.add_right_cancel_iff`, states that for any type `α` with an addition (`Add α`) operation, and for any three elements `a`, `b`, `c` of the type `WithTop α` (which is the type `α` with a special element `⊤` attached), the following holds: if `a` is not equal to `⊤` and the type `α` has the right-cancellation property with respect to addition (`IsRightCancelAdd α`), then the equality `b + a = c + a` implies `b = c`, and conversely, `b = c` implies `b + a = c + a`. In other words, one can cancel `a` from both sides of an equation if `a` is not the special `⊤` element and the addition operation is right-cancellable.
More concisely: If `α` is a type with an addition operation and `WithTop α` has right-cancellation for addition, then for all `a, b, c ∈ WithTop α` with `a ≠ ⊤`, `a` being the special element in `WithTop α`, the equations `b + a = c + a` and `b = c` are equivalent.
|
WithTop.add_top
theorem WithTop.add_top : ∀ {α : Type u} [inst : Add α] (a : WithTop α), a + ⊤ = ⊤
The theorem `WithTop.add_top` states that for any given type `α` that has an addition operation (denoted by `Add α`) and any instance `a` of the type `WithTop α` (which is type `α` plus an extra top element `⊤`), the sum of `a` and `⊤` is always equal to `⊤`. Essentially, `⊤` behaves like an absorbing element for the addition operation in this context.
More concisely: For any type `α` with an addition operation and instance `WithTop α` having top element `⊤`, the addition of any element `a ∈ α` with `⊤` results in `⊤`. In mathematical notation, `a + ⊤ = ⊤` for all `a ∈ α`.
|
WithTop.add_lt_add_right
theorem WithTop.add_lt_add_right :
∀ {α : Type u} [inst : Add α] {a b c : WithTop α} [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 → b + a < c + a
This theorem, `WithTop.add_lt_add_right`, states that for any type `α` that has an addition operation and a less than operation, and for any three elements `a`, `b`, and `c` of the type `α` with the special top element `⊤` added, if `a` is not equal to `⊤` and `b` is less than `c`, then the result of adding `a` to `b` is less than the result of adding `a` to `c`. It requires that `α` has a covariant class, meaning the order is preserved when the parameters of the function `x + x_1` are swapped. In mathematical terms, it is essentially stating that if `a ≠ ∞` and `b < c`, then `b + a < c + a`, where `a`, `b`, and `c` are elements in an ordered semigroup.
More concisely: For any ordered semigroup with covariant order, if `a` is not the top element and `b` is less than `c`, then `a + b` is less than `a + c`.
|
WithTop.coe_one
theorem WithTop.coe_one : ∀ {α : Type u} [inst : One α], ↑1 = 1
This theorem states that for any type `α` that has a multiplicative identity (or "one" element), the embedding of the identity element of `α` into the extended type `WithTop α` (which adds an additional "top" element to `α`) is equal to the identity of `WithTop α`. In simpler terms, it asserts that the "one" of `α` is the same as the "one" in its extended type `WithTop α`.
More concisely: For any type `α` with a multiplicative identity, the identity element of `α` is equal to the multiplicative identity in the extended type `WithTop α`.
|
WithTop.zero_lt_top
theorem WithTop.zero_lt_top : ∀ {α : Type u} [inst : OrderedAddCommMonoid α], 0 < ⊤
This theorem, `WithTop.zero_lt_top`, states that for any ordered additive commutative monoid `α`, zero is less than infinity. An ordered additive commutative monoid is a mathematical structure that combines the properties of an ordered set (i.e., it has a notion of "less than"), a commutative monoid (it has an operation that is associative and commutative, and also has an identity element), and the operation also respects the order. The symbol `⊤` represents infinity in this context.
More concisely: In any ordered additive commutative monoid, zero is less than the infinite element.
|
WithTop.coe_eq_zero
theorem WithTop.coe_eq_zero : ∀ {α : Type u} [inst : Zero α] {a : α}, ↑a = 0 ↔ a = 0
This theorem, `WithTop.coe_eq_zero`, states that for any type `α` that has a zero element, the equality holds between the lifted value `↑a = 0` and the original value `a = 0`. In other words, the element `a` of type `α` is zero if and only if its lifted version (via `WithTop.coe`, which injects `α` into `WithTop α`) is also zero.
More concisely: For any type `α` with a zero element, the lifted value `WithTop.coe a` equals zero if and only if the original value `a` is zero.
|
WithTop.coe_zero
theorem WithTop.coe_zero : ∀ {α : Type u} [inst : Zero α], ↑0 = 0
This theorem states that for all types `α` that have a zero (`0`) element, the coerced value of `0` (`↑0`) in the `WithTop` wrapper is equal to `0`. In simpler terms, it shows that zero wrapped with `WithTop` is still zero. This fact is true regardless of what type `α` is, as long as `α` has a defined zero.
More concisely: For all types `α` with a zero element, the `WithTop` wrapper of `0` equals `0`. (Or, in mathematical notation, `↑0 = 0` where `α` has `0`.)
|
WithBot.add_eq_bot
theorem WithBot.add_eq_bot : ∀ {α : Type u} [inst : Add α] {a b : WithBot α}, a + b = ⊥ ↔ a = ⊥ ∨ b = ⊥
The theorem `WithBot.add_eq_bot` states that, for any type `α` that has an addition operation, and any two objects `a` and `b` of the type `WithBot α` (which extends `α` by attaching the bottom element `⊥`), the sum `a + b` equals to `⊥` if and only if either `a` is `⊥` or `b` is `⊥`. This theorem captures the intuition that in any addition operation, if one of the elements is considered as the "bottom" or undefined element, the result is also the "bottom" or undefined.
More concisely: For any type `α` with addition and any `WithBot α` elements `a` and `b`, `a + b = ⊥` if and only if `a = ⊥` or `b = ⊥`.
|
WithTop.coe_add
theorem WithTop.coe_add : ∀ {α : Type u} [inst : Add α] (a b : α), ↑(a + b) = ↑a + ↑b
This theorem states that for any type `α` that has an addition operation (`Add α`), the addition of two elements `a` and `b` of type `α` lifted to the `WithTop` type (denoted by `↑(a + b)`) is equal to the sum of the lifted elements `a` and `b` (denoted by `↑a + ↑b`). In other words, the lifting operation commutes with the addition operation.
More concisely: For any type `α` with an addition operation and for all `a` and `b` in `α`, the lifted addition `↑(a + b)` equals the sum of the lifted elements `↑a + ↑b`.
|
Mathlib.Algebra.Order.Monoid.WithTop._auxLemma.21
theorem Mathlib.Algebra.Order.Monoid.WithTop._auxLemma.21 :
∀ {α : Type u} [inst : Add α] {a b : WithTop α}, (a + b = ⊤) = (a = ⊤ ∨ b = ⊤)
This theorem states that for any given type `α` which has an addition operation (`Add α`), and for any two elements `a` and `b` of the type `WithTop α` (which is essentially the type `α` plus an additional element `⊤`), the sum `a + b` equals `⊤` if and only if either `a` equals `⊤` or `b` equals `⊤`.
More concisely: For any type `α` with addition and for any `a, b ∈ WithTop α`, the sum `a + b` equals `⊤` if and only if `a = ⊤` or `b = ⊤`.
|
WithTop.add_left_cancel_iff
theorem WithTop.add_left_cancel_iff :
∀ {α : Type u} [inst : Add α] {a b c : WithTop α} [inst_1 : IsLeftCancelAdd α], a ≠ ⊤ → (a + b = a + c ↔ b = c)
This theorem states that for any type `α` equipped with an addition operation and the property that addition is left-cancellable (i.e., for any `x`, `y`, and `z` in `α`, if `x + y = x + z` then `y = z`), and any three values `a`, `b`, and `c` in the type `α` extended with a top element (denoted `WithTop α`), if `a` is not the top element, then the equality `a + b = a + c` holds if and only if `b = c`. In other words, addition is also left-cancellable in the extended type `WithTop α`, as long as we're not adding to the top element.
More concisely: For any type `α` with left-cancellative addition and a top element, the equality `a + b = a + c` in `WithTop α` holds if and only if `b = c`, provided `a` is not the top element.
|
WithTop.le_of_add_le_add_left
theorem WithTop.le_of_add_le_add_left :
∀ {α : Type u} [inst : Add α] {a b c : WithTop α} [inst_1 : LE α]
[inst_2 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], a ≠ ⊤ → a + b ≤ a + c → b ≤ c
The theorem `WithTop.le_of_add_le_add_left` states that for any type `α` with addition (`Add α`), an order (`LE α`), and a contravariant class - where addition of any two elements is less than or equal to the sum of two other elements - if we have three elements `a`, `b`, and `c` of the type `α` extended with `⊤` (`WithTop α`), and `a` is not top (`⊤`), then if `a + b` is less than or equal to `a + c`, it follows that `b` is less than or equal to `c`. This is essentially a property of 'cancellation' for addition in this context, resembling the property of the integers.
More concisely: If `α` is a type with an order and additions, and `a, b, c` are elements of `α` with `a ≠ ⊤`, then `a + b ≤ a + c` implies `b ≤ c`.
|
WithTop.top_add
theorem WithTop.top_add : ∀ {α : Type u} [inst : Add α] (a : WithTop α), ⊤ + a = ⊤
The theorem `WithTop.top_add` states that for any type `α` that has an addition operation defined on it, when you add the special element `⊤` (representing a kind of "infinity") to any element `a` of the type `WithTop α` (which is `α` with an additional `⊤` element), the result is always `⊤`. This means that `⊤` acts as an absorbing element for the addition operation in the extended type `WithTop α`.
More concisely: For any type `α` with an addition operation, in `WithTop α`, the element `⊤` absorbs additions, i.e., `a + ⊤ = ⊤` for all `a` in `α`.
|
WithTop.add_eq_top
theorem WithTop.add_eq_top : ∀ {α : Type u} [inst : Add α] {a b : WithTop α}, a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤
The theorem `WithTop.add_eq_top` states that for any type `α` endowed with an addition operation and any two elements `a` and `b` of the type `WithTop α` (which is the type `α` extended with an additional element `⊤`), the sum `a + b` equals to `⊤` if and only if either `a` equals `⊤` or `b` equals `⊤`. In other words, in the extended type `WithTop α`, the only way you can get `⊤` as the result of addition operation is if at least one of the operands is `⊤` itself.
More concisely: In the type `WithTop α`, for any `α` with addition operation, `a + b = ⊤` if and only if `a = ⊤` or `b = ⊤`.
|
WithBot.coe_eq_zero
theorem WithBot.coe_eq_zero : ∀ {α : Type u} [inst : Zero α] {a : α}, ↑a = 0 ↔ a = 0
This theorem states that for any type `α` that has a `Zero` instance, and any instance `a` of that type, the lift of `a` to the type `WithBot α` equals zero if and only if `a` equals zero itself. In other words, an element is equivalent to zero in `WithBot α` (which is `α` along with an additional bottom element) if and only if it is zero in `α`.
More concisely: For any type `α` with a `Zero` instance and any `a : α`, `lift a to WithBot α = zero (WithBot α) <--> a = zero α`.
|
WithTop.le_of_add_le_add_right
theorem WithTop.le_of_add_le_add_right :
∀ {α : Type u} [inst : Add α] {a b c : WithTop α} [inst_1 : LE α]
[inst_2 : ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1],
a ≠ ⊤ → b + a ≤ c + a → b ≤ c
This theorem states that for any type `α` equipped with an addition operation and a less than or equal to relation, if the addition operation and the less than or equal to relation are related by the contravariant class relation with the swap of addition operation, then for any three elements `a`, `b`, and `c` of the type `α` or the special element `⊤` (coming from the `WithTop` construction), if `a` is not `⊤` and `b` plus `a` is less than or equal to `c` plus `a`, then `b` is less than or equal to `c`. In other words, it's saying if we add the same non-top element to two elements, and it doesn't change the order of the elements, then the two elements must have been in that same order to begin with.
More concisely: If `α` is a type with an addition operation and a less than or equal to relation such that addition is opposite-preserving with respect to the less than or equal to relation, then for all `a, b, c` in `α` or the top element `⊤`, if `a ≠ ⊤` and `a + b ≤ a + c`, then `b ≤ c`.
|
WithBot.coe_zero
theorem WithBot.coe_zero : ∀ {α : Type u} [inst : Zero α], ↑0 = 0
This theorem states that for any type `α` that has an instance of the `Zero` typeclass (meaning it has a defined 'zero' value), the 'coercion' or typecast of the zero value of `α` (`↑0`) results in the zero value in the `WithBot` structure (`0`). In other words, when zero of any type with a defined zero is lifted to the `WithBot` type, it remains zero.
More concisely: For any type `α` with a `Zero` instance, the coercion of its zero value to the `WithBot` type results in the `WithBot` zero value. In other words, `↑0 : WithBot α = 0 : WithBot`.
|
WithBot.add_bot
theorem WithBot.add_bot : ∀ {α : Type u} [inst : Add α] (a : WithBot α), a + ⊥ = ⊥
This theorem, `WithBot.add_bot`, states that for any type `α` with an addition operation (`Add α`), if you take an element `a` from the type `α` extended with a `⊥` value (`WithBot α`), then adding this `a` to `⊥` always results in `⊥`. In other words, whenever we add the special `⊥` value to any element in the extended type, the result is always `⊥`. This is similar to the behavior of `NaN` or Not-a-Number in some programming languages, where any arithmetic operation involving `NaN` yields `NaN`.
More concisely: For any type `α` with addition and any `a ∈ WithBot α`, `a + ⊥ = ⊥`.
|
WithBot.coe_one
theorem WithBot.coe_one : ∀ {α : Type u} [inst : One α], ↑1 = 1
This theorem states that for any type `α` with a defined `One` instance (indicating that the type has a concept of the number one), the coercion of 1 (as a number in that type) to the type "with bottom" (`WithBot`) equals 1. The "with bottom" type is typically used to add a least element (often called "bottom" or ⊥) to a type that doesn't necessarily have a natural least element. So, this theorem is essentially saying that 1 stays the same even when we consider it in the context of a type that includes a bottom element.
More concisely: For any type `α` with a defined `One` instance, the coercion of `1` to `α WithBot` equals `1`.
|
WithTop.one_ne_top
theorem WithTop.one_ne_top : ∀ {α : Type u} [inst : One α], 1 ≠ ⊤
This theorem states that for any given type `α`, assuming that `α` has an identity element under multiplication (denoted as `1`), the identity element `1` is not equal to the top element, denoted as `⊤`. In other words, within the context of an algebraic structure where a multiplicative identity exists, that identity cannot be considered the top or maximum element.
More concisely: In any algebraic structure with a multiplicative identity, the identity element is distinct from the top element.
|
Mathlib.Algebra.Order.Monoid.WithTop._auxLemma.2
theorem Mathlib.Algebra.Order.Monoid.WithTop._auxLemma.2 : ∀ {α : Type u} [inst : Zero α] {a : α}, (↑a = 0) = (a = 0)
This theorem, `Mathlib.Algebra.Order.Monoid.WithTop._auxLemma.2`, states that for any type `α` that has a `Zero` instance and a given element `a` of this type, the equality of the lifted value of `a` to the zero element is equivalent to the equality of `a` itself to the zero element. In other words, if we lift `a` into the `WithTop` type (which adds a "top" element to a given type), stating that `a` equals zero in this extended type is the same as saying that `a` equals zero in its original type.
More concisely: For any type `α` with a `Zero` instance, the lifted value of an element `a` in `α` equals the zero element in the `WithTop` type if and only if `a` equals the zero element in `α`.
|
WithTop.add_lt_add_left
theorem WithTop.add_lt_add_left :
∀ {α : Type u} [inst : Add α] {a b c : WithTop α} [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 < a + c
This theorem states that for any type `α` implementing addition (`Add α`) and a less-than relation (`LT α`), and for any three elements `a`, `b`, and `c` of the type `WithTop α` (which represents the original type `α` augmented with an additional `top` element), if the `a` is not the `top` element (`a ≠ ⊤`) and `b` is less than `c` (`b < c`), then adding `a` to `b` is less than adding `a` to `c` (`a + b < a + c`). This is under the assumption that the type `α` satisfies the `CovariantClass` property with respect to the addition and less-than operations, which essentially requires the addition operation to be monotonic with respect to the less-than relation.
More concisely: For types `α` with `Add α` and `LT α` such that `α` satisfies the `CovariantClass` property, if `a ≠ ⊤` and `b < c` in `WithTop α`, then `a + b < a + c`.
|
Mathlib.Algebra.Order.Monoid.WithTop._auxLemma.41
theorem Mathlib.Algebra.Order.Monoid.WithTop._auxLemma.41 :
∀ {α : Type u} [inst : Zero α] {a : α}, (↑a = 0) = (a = 0)
This theorem, `Mathlib.Algebra.Order.Monoid.WithTop._auxLemma.41`, states that for any type `α` that has an instance of `Zero`, and for any element `a` of that type, the condition of `a` being equal to zero when lifted to the "with top" monoid (denoted as `↑a`) is equivalent to `a` being zero in the original type. In other words, `a` is zero in `α` if and only if its lift, `↑a`, is zero in the "with top" monoid.
More concisely: For any type `α` with a `Zero` instance and any `a` in `α`, `a` is equal to zero in `α` if and only if `↑a` is zero in the "with top" monoid of `α`.
|