WithTop.mul_top
theorem WithTop.mul_top :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a : WithTop α}, a ≠ 0 → a * ⊤ = ⊤
This theorem states that for any type `α` which has decidable equality and a multiplication operation that includes a zero element, a non-zero element `a` of the extended type 'WithTop α' (which includes the original type `α` and an additional top element `⊤`), the product of `a` and `⊤` is `⊤`. The result `⊤` can be thought of as an "infinity" or "undefined" value, thus, this theorem essentially states that any non-zero number multiplied by infinity equals infinity.
More concisely: For any type `α` with decidable equality and a multiplicative identity `⊤`, the product of a non-zero element `a` in `α` and the top element `⊤` in `WithTop α` equals the top element `⊤`.
|
WithBot.mul_bot
theorem WithBot.mul_bot :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a : WithBot α}, a ≠ 0 → a * ⊥ = ⊥
The theorem `WithBot.mul_bot` asserts that for any type `α` (where `α` has decidable equality and is a multiplication-zero class), and any element `a` of the type `WithBot α` (which is `α` extended with a "bottom" element), if `a` is not zero then the product of `a` and the bottom element is the bottom element. In other words, for any non-zero element in an extended type, multiplication with the added bottom element results in the bottom element. This is akin to the principle that any number except zero, when multiplied with infinity (or an undefined value), results in an undefined value or infinity.
More concisely: For any type `α` with decidable equality and multiplication-zero class, and any non-zero element `a` in the extended type `WithBot α`, `a * ⊥ = ⊥`, where `⊥` denotes the bottom element.
|
WithTop.top_mul
theorem WithTop.top_mul :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {b : WithTop α}, b ≠ 0 → ⊤ * b = ⊤
The `WithTop.top_mul` theorem states that for any type `α` that has a decidable equality and a multiplication operation with a zero, if we extend this type `α` to include a top element `⊤` (which we do by using `WithTop α`), then the product of the `⊤` and any element `b` of this extended type, provided `b` is not zero, is also `⊤`. This property is similar to some properties of infinity in mathematics, where, barring exceptions, the product of infinity and any non-zero number is still infinity.
More concisely: If `α` is a type with decidable equality and a multiplication operation with a zero, then in the extended type `WithTop α`, `⊤ * b = ⊤` for all `b ≠ 0` in `α`.
|
WithTop.mul_lt_top'
theorem WithTop.mul_lt_top' :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : LT α] {a b : WithTop α},
a < ⊤ → b < ⊤ → a * b < ⊤
The theorem `WithTop.mul_lt_top'` states that for any type `α` that has a decidable equality relation, a multiplication operation that respects zero (`MulZeroClass α`), and a less than relation (`LT α`), if `a` and `b` are elements of the type that includes `α` and an additional top element (`WithTop α`), and both `a` and `b` are less than this top element, then the product of `a` and `b` is also less than the top element. Essentially, this theorem guarantees that for two elements less than the top element in a `WithTop` structure with these properties, their multiplication will also stay within the bounds of the set and be less than the top element.
More concisely: For any type `α` with decidable equality, `MulZeroClass α`, and `LT α`, in a `WithTop α`, if `a` and `b` are less than the top element, then their product `a * b` is also less than the top element.
|
WithTop.coe_mul
theorem WithTop.coe_mul :
∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] (a b : α), ↑(a * b) = ↑a * ↑b
The theorem `WithTop.coe_mul` states that for any type `α`, given that `α` has decidable equality property (`DecidableEq α`) and zero multiplication class property (`MulZeroClass α`), for all elements `a` and `b` of type `α`, the operation of multiplication of `a` and `b` then coercing the result to "WithTop α" is equivalent to the operation of coercing `a` and `b` to "WithTop α" first and then multiplying them. In other words, the order of multiplication and coercion operation doesn't affect the final result. This theorem is about the preservation of multiplication operation under the coercion to "WithTop α".
More concisely: For any type `α` with decidable equality and zero multiplication, the operation of coercing `α` elements to "WithTop α" and then multiplying is equivalent to multiplying and then coercing to "WithTop α".
|