LinearOrderedCancelCommMonoid.le_total
theorem LinearOrderedCancelCommMonoid.le_total :
∀ {α : Type u_3} [self : LinearOrderedCancelCommMonoid α] (a b : α), a ≤ b ∨ b ≤ a
The theorem `LinearOrderedCancelCommMonoid.le_total` states that for any type `α` that forms a `LinearOrderedCancelCommMonoid`, for any two values `a` and `b` of this type, either `a` is less than or equal to `b` or `b` is less than or equal to `a`. In other words, it confirms the totality of the linear order, indicating that any pair of elements in this set is comparable.
More concisely: In a LinearOrderedCancelCommMonoid, any two elements are comparable in the linear order.
|
LinearOrderedCancelCommMonoid.min_def
theorem LinearOrderedCancelCommMonoid.min_def :
∀ {α : Type u_3} [self : LinearOrderedCancelCommMonoid α] (a b : α), min a b = if a ≤ b then a else b
This theorem states that for any two elements `a` and `b` of a type `α`, which is a Linear Ordered Cancel Commutative Monoid, the `min` function (which returns the minimum of `a` and `b`) is equivalent to the function `minOfLe`, which returns `a` if `a` is less than or equal to `b`, and `b` otherwise. In other words, `min a b` will always return the same result as `if a ≤ b then a else b` in this algebraic structure.
More concisely: For any type `α` being a Linear Ordered Cancel Commutative Monoid, the function `min` and the function `minOfLe` defined as `if _ <= _ then _ else _` are equivalent for any two elements `a` and `b`: `min a b = if a <= b then a else b`.
|
add_top
theorem add_top : ∀ {α : Type u_1} [inst : LinearOrderedAddCommMonoidWithTop α] (a : α), a + ⊤ = ⊤
This theorem states that for any type `α` that has a structure of a `LinearOrderedAddCommMonoidWithTop`, the sum of any element `a` of type `α` and the top element `⊤` is always `⊤`. In other words, adding anything to the maximum possible value in this ordered, add-commutative monoid still results in the maximum possible value.
More concisely: For any type `α` with a `LinearOrderedAddCommMonoidWithTop` structure, `a + ⊤ = ⊤` for all elements `a` of type `α`.
|
LinearOrderedCommMonoid.min_def
theorem LinearOrderedCommMonoid.min_def :
∀ {α : Type u_3} [self : LinearOrderedCommMonoid α] (a b : α), min a b = if a ≤ b then a else b
This theorem states that for any type `α` that is a linearly ordered commutative monoid, the minimum function `min` for any two elements `a` and `b` of that type is defined as follows: if `a` is less than or equal to `b`, then the minimum is `a`, else, the minimum is `b`.
More concisely: For any linearly ordered commutative monoid type `α`, the minimum function `min` is defined as `a` for `a ≤ b` and `b` otherwise.
|
Mathlib.Algebra.Order.Monoid.Defs._auxLemma.2
theorem Mathlib.Algebra.Order.Monoid.Defs._auxLemma.2 :
∀ {α : Type u_1} [inst : LinearOrderedAddCommMonoid α] {a : α}, (0 ≤ a + a) = (0 ≤ a)
This theorem, known as `_auxLemma.2` from the `Mathlib.Algebra.Order.Monoid.Defs` module, applies to any type `α` that forms a linearly ordered additive commutative monoid. The theorem states that for any element `a` of this type, the property that `0` is less than or equal to `a + a` (i.e., twice `a`) is equivalent to the property that `0` is less than or equal to `a` itself.
More concisely: For any linearly ordered additive commutative monoid type `α`, the element `0` is less than or equal to `2*a` if and only if it is less than or equal to `a`.
|
LinearOrderedCommMonoid.le_total
theorem LinearOrderedCommMonoid.le_total :
∀ {α : Type u_3} [self : LinearOrderedCommMonoid α] (a b : α), a ≤ b ∨ b ≤ a
This theorem states that for any given type 'α' that is a Linear Ordered Commutative Monoid, and for any two elements 'a' and 'b' of that type, one of the elements is less than or equal to the other. In other words, either 'a' is less than or equal to 'b', or 'b' is less than or equal to 'a'; this property is also known as 'totality' in order theory.
More concisely: For any Linear Ordered Commutative Monoid type 'α', every two elements 'a' and 'b' have a relation whereby one is less than or equal to the other.
|
LinearOrderedCommMonoid.max_def
theorem LinearOrderedCommMonoid.max_def :
∀ {α : Type u_3} [self : LinearOrderedCommMonoid α] (a b : α), max a b = if a ≤ b then b else a
This theorem states that for any type `α` which has the structure of a `LinearOrderedCommMonoid`, the maximum of two elements `a` and `b` can be defined in terms of the `if-then-else` construct. Specifically, the maximum of `a` and `b` is `b` if `a` is less than or equal to `b`, and otherwise it's `a`.
More concisely: For any type `α` with a LinearOrderedCommMonoid structure, the maximum of two elements `a` and `b` is defined as `if a <= b then b else a`.
|
LinearOrderedCancelCommMonoid.compare_eq_compareOfLessAndEq
theorem LinearOrderedCancelCommMonoid.compare_eq_compareOfLessAndEq :
∀ {α : Type u_3} [self : LinearOrderedCancelCommMonoid α] (a b : α), compare a b = compareOfLessAndEq a b := by
sorry
The theorem `LinearOrderedCancelCommMonoid.compare_eq_compareOfLessAndEq` states that for any type `α` that is a `LinearOrderedCancelCommMonoid` (a structure that combines properties of a commutative monoid, a cancelative monoid, and a total order), the comparison of two elements `a` and `b` using the `compare` function is equivalent to comparing them using the `compareOfLessAndEq` function, provided we have methods for deciding whether `a` is less than `b` and whether `a` equals `b`. In other words, `compare a b` produces the same result as `compareOfLessAndEq a b` for any elements `a` and `b` of `α`.
More concisely: For any type `α` that is a LinearOrderedCancelCommMonoid, the comparison functions `compare` and `compareOfLessAndEq` agree on `α`.
|
LinearOrderedAddCommMonoid.min_def
theorem LinearOrderedAddCommMonoid.min_def :
∀ {α : Type u_3} [self : LinearOrderedAddCommMonoid α] (a b : α), min a b = if a ≤ b then a else b
This theorem states that for any type `α` that is a Linear Ordered Additive Commutative Monoid (meaning it has operations of addition and order that obey certain properties), the minimum function `min` between any two elements `a` and `b` of type `α` is defined as follows: if `a` is less than or equal to `b`, then the minimum is `a`, otherwise it's `b`.
More concisely: For any Linear Ordered Additive Commutative Monoid type `α`, the minimum function `min` is defined as `if a ≤ b then a else b`, where `a` and `b` are elements of `α`.
|
LinearOrderedAddCommMonoid.le_total
theorem LinearOrderedAddCommMonoid.le_total :
∀ {α : Type u_3} [self : LinearOrderedAddCommMonoid α] (a b : α), a ≤ b ∨ b ≤ a
This theorem states that in a linearly ordered additive commutative monoid, given any two elements `a` and `b`, either `a` is less than or equal to `b` or `b` is less than or equal to `a`. This property is known as totality, which is characteristic of linear orders. In mathematical notation, for all `a` and `b` in the monoid `α`, we have `a ≤ b ∨ b ≤ a`.
More concisely: In a linearly ordered additive commutative monoid, every two elements are comparable.
|
LinearOrderedCancelAddCommMonoid.compare_eq_compareOfLessAndEq
theorem LinearOrderedCancelAddCommMonoid.compare_eq_compareOfLessAndEq :
∀ {α : Type u_3} [self : LinearOrderedCancelAddCommMonoid α] (a b : α), compare a b = compareOfLessAndEq a b := by
sorry
This theorem states that, for any arbitrary type `α` that has the structure of a `LinearOrderedCancelAddCommMonoid`, i.e., a commutative monoid with a linear order and cancellation properties, the `compare` function and `compareOfLessAndEq` function yield the same results. In other words, the comparison of any two elements `a` and `b` of this `α` using the `compare` function is identical to the comparison results obtained by using the `compareOfLessAndEq` function, provided the type `α` is decidable for `<` and `=`. Here, `compare` function provides an `Ordering` such that `a < b` corresponds to `Ordering.lt`, `a = b` corresponds to `Ordering.eq`, and otherwise, it corresponds to `Ordering.gt`.
More concisely: For any decidably ordered, commutative monoid `α` with cancellation properties, the `compare` and `compareOfLessAndEq` functions give identical results on elements of `α`.
|
LinearOrderedAddCommMonoid.max_def
theorem LinearOrderedAddCommMonoid.max_def :
∀ {α : Type u_3} [self : LinearOrderedAddCommMonoid α] (a b : α), max a b = if a ≤ b then b else a
The theorem states that for any type `α` that has the structure of a `LinearOrderedAddCommMonoid`, the maximum function `max` applied to any two elements `a` and `b` of type `α` produces an output equivalent to the result of a conditional statement: if `a` is less than or equal to `b`, it returns `b`; otherwise, it returns `a`. This aligns with the intuitive understanding of the maximum function: it returns the larger of the two inputs.
More concisely: For any type `α` with a LinearOrderedAddCommMonoid structure, `max a b = if a ≤ b then b else a`.
|
top_add
theorem top_add : ∀ {α : Type u_1} [inst : LinearOrderedAddCommMonoidWithTop α] (a : α), ⊤ + a = ⊤
This theorem states that for any type `α` that is a linearly ordered additive commutative monoid with a top element (denoted ⊤), the sum of the top element and any other element `a` from the same type `α` is always the top element. In other words, if we add any element to the maximum possible element (top) in such a structure, the result will always be the top element itself.
More concisely: For any linearly ordered additive commutative monoid `α` with a top element ⊤, the sum of any element `a` from `α` and the top element is equal to the top element. (∀α : Type, LinearlyOrderedAddCommMonoid α ∧ TopElement α α ⊤ → α → α, ∀a, a ⊔ ⊤ = ⊤)
|
LinearOrderedAddCommMonoidWithTop.top_add'
theorem LinearOrderedAddCommMonoidWithTop.top_add' :
∀ {α : Type u_3} [self : LinearOrderedAddCommMonoidWithTop α] (x : α), ⊤ + x = ⊤
This theorem states that, in a linearly ordered additive commutative monoid that has a top element, the top element remains unchanged when added to any other element in the set. In terms of mathematical symbols, for any element 'x' within such a structure, adding 'x' to the top element (denoted as '⊤') will yield '⊤'.
More concisely: In a linearly ordered additive commutative monoid with a top element, adding any element to the top element results in the top element.
|
LinearOrderedCommMonoid.compare_eq_compareOfLessAndEq
theorem LinearOrderedCommMonoid.compare_eq_compareOfLessAndEq :
∀ {α : Type u_3} [self : LinearOrderedCommMonoid α] (a b : α), compare a b = compareOfLessAndEq a b
This theorem asserts that, for any linear ordered commutative monoid (which is a type `α` with specific properties), the comparison of any two elements `a` and `b` using the `compare` function will yield the same result as comparing them with the `compareOfLessAndEq` function. In other words, the `compare` function and the `compareOfLessAndEq` function are equivalent when used on elements of a linear ordered commutative monoid. This equivalence holds true for every `a` and `b` within `α`, i.e., it is universally quantified over `α`.
More concisely: For all linear ordered commutative monoids α, the comparison function compare on elements a and b is equal to compareOfLessAndEq on a and b.
|
LinearOrderedCancelCommMonoid.max_def
theorem LinearOrderedCancelCommMonoid.max_def :
∀ {α : Type u_3} [self : LinearOrderedCancelCommMonoid α] (a b : α), max a b = if a ≤ b then b else a
This theorem states that for any linearly ordered cancellative commutative monoid (a type of algebraic structure), the maximum function behaves in a certain way. Specifically, given any two elements `a` and `b` from this monoid, the maximum of `a` and `b` is defined as `b` if `a` is less than or equal to `b`, otherwise it is `a`.
More concisely: For any linearly ordered cancellative commutative monoid, the maximum function is defined as the larger of the two elements.
|
LinearOrderedCancelAddCommMonoid.le_total
theorem LinearOrderedCancelAddCommMonoid.le_total :
∀ {α : Type u_3} [self : LinearOrderedCancelAddCommMonoid α] (a b : α), a ≤ b ∨ b ≤ a
This theorem states that for any two elements `a` and `b` of a type `α`, where `α` is a linearly ordered cancelable commutative monoid, either `a` is less than or equal to `b` or `b` is less than or equal to `a`. In simpler terms, it states that in such a monoid, any two elements are in a total order relationship, which means that for any two elements, one of them is less than or equal to the other.
More concisely: In a linearly ordered, cancelable commutative monoid, any two elements are comparable.
|
LinearOrderedCancelAddCommMonoid.min_def
theorem LinearOrderedCancelAddCommMonoid.min_def :
∀ {α : Type u_3} [self : LinearOrderedCancelAddCommMonoid α] (a b : α), min a b = if a ≤ b then a else b
This theorem states that for any type `α` that is part of the `LinearOrderedCancelAddCommMonoid` class, the minimum function `min` between two elements `a` and `b` of type `α` is equivalent to a function that checks if `a` is less than or equal to `b`; if this condition is true then it returns `a`, otherwise it returns `b`. This is a property of ordered additive commutative monoids where addition is cancellable.
More concisely: For any type `α` in the `LinearOrderedCancelAddCommMonoid` class, the function `min` between two elements `a` and `b` is equal to the function that returns `a` if `a` ≤ `b`, and `b` otherwise.
|
LinearOrderedCancelAddCommMonoid.max_def
theorem LinearOrderedCancelAddCommMonoid.max_def :
∀ {α : Type u_3} [self : LinearOrderedCancelAddCommMonoid α] (a b : α), max a b = if a ≤ b then b else a
This theorem states that in the context of a linearly ordered cancelable additive commutative monoid (`LinearOrderedCancelAddCommMonoid`), the maximum function (`max`) for any two elements `a` and `b` is defined as follows: if `a` is less than or equal to `b` then the result is `b`, otherwise the result is `a`. In essence, the `max` function is using the `≤` comparison to determine the maximum of two elements.
More concisely: In a linearly ordered, cancelable, additive, commutative monoid, max(a, b) = a if a > b, and max(a, b) = b otherwise.
|
LinearOrderedAddCommMonoid.compare_eq_compareOfLessAndEq
theorem LinearOrderedAddCommMonoid.compare_eq_compareOfLessAndEq :
∀ {α : Type u_3} [self : LinearOrderedAddCommMonoid α] (a b : α), compare a b = compareOfLessAndEq a b
This theorem states that, for any type `α` that forms a `LinearOrderedAddCommMonoid` (this is a structure that combines the properties of being a monoid under addition, and a linear order), the comparison of two elements `a` and `b` of type `α`, using the built-in comparison function `compare`, gives the same result as the comparison using the function `compareOfLessAndEq`. The function `compareOfLessAndEq` returns an ordering (`Ordering.lt`, `Ordering.eq`, or `Ordering.gt`) based on comparisons made using the less than (`<`) operator and equality (`=`).
More concisely: For any type `α` that is a LinearOrderedAddCommMonoid, the comparison function `compare` and the function `compareOfLessAndEq` based on `<` and `=` agree on their results.
|