ENNReal.cancel_of_lt'
theorem ENNReal.cancel_of_lt' : ∀ {a b : ENNReal}, a < b → AddLECancellable a
This theorem, labeled as "ENNReal.cancel_of_lt'", states that for any two elements `a` and `b` from the set of extended nonnegative real numbers (denoted as `[0, ∞]`), if `a` is strictly less than `b`, then `a` is `AddLECancellable`. In mathematical terms, an element `a` is considered `AddLECancellable` if for all `b` and `c` in the set, if `a + b` is less than or equal to `a + c`, then `b` is less than or equal to `c`. This essentially means that adding `a` to two different values maintains the order between those two values.
More concisely: For all `a` and `b` in `[0, ∞]` with `a < b`, `a` is `AddLECancellable`. In other words, if `a` is a strictly positive element in the extended nonnegative real numbers, then adding `a` to two different numbers preserves the order between them.
|
ENNReal.mul_lt_mul_left
theorem ENNReal.mul_lt_mul_left : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → (a * b < a * c ↔ b < c)
This theorem states that for all extended nonnegative real numbers `a`, `b`, and `c`, if `a` is neither zero nor infinity (`⊤` represents infinity in this context), then `a` multiplied by `b` is less than `a` multiplied by `c` if and only if `b` is less than `c`. In other words, if `a` is a positive, finite extended nonnegative real number, then multiplication by `a` preserves the order of `b` and `c`.
More concisely: For all extended nonnegative real numbers `a` neither zero nor infinity, `a * b` < `a * c` if and only if `b` < `c`.
|
ENNReal.toNNReal_sum
theorem ENNReal.toNNReal_sum :
∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal},
(∀ a ∈ s, f a ≠ ⊤) → (s.sum fun a => f a).toNNReal = s.sum fun a => (f a).toNNReal
This theorem states that for any given type `α`, any finite set `s` of elements of type `α`, and any function `f` that maps elements of `α` to extended nonnegative real numbers (`ENNReal`), as long as none of the `ENNReal` values generated by `f` for elements in `s` is infinity (notated as `⊤`), the sum of those `ENNReal` values, when viewed as nonnegative real numbers (`NNReal`), is equal to the sum of the `NNReal` values that those `ENNReal` values correspond to. In mathematical terms, this can be written as:
For all α, s and f where f: α → `[0, ∞]` such that for all a in s, f(a) ≠ ∞, the sum over s of f(a) viewed as `ℝ≥0` is equal to the sum over s of f(a) viewed as `ℝ≥0∞`.
More concisely: For any type `α`, finite set `s` of `α` elements, and function `f:` `α` `→` `[0, ∞]` such that `f(a)` is finite for all `a` in `s`, the sum of `f(a)` as non-negative real numbers equals the sum of the non-negative real numbers represented by `f(a)`.
|
ENNReal.top_sub_coe
theorem ENNReal.top_sub_coe : ∀ {r : NNReal}, ⊤ - ↑r = ⊤
This theorem, in the `ENNReal` namespace, states that for every nonnegative real number `r` (represented as `NNReal`), the difference between the extended real number positive infinity (denoted as `⊤`) and the real number `r` is still positive infinity. Essentially, it is saying that subtracting any nonnegative real number from positive infinity still results in positive infinity. This is a special case of the more general theorem `WithTop.top_sub_coe`.
More concisely: For every nonnegative real number `r`, `r < ⊤` implies `⊤ - r = ⊤`.
|
ENNReal.lt_add_right
theorem ENNReal.lt_add_right : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ 0 → a < a + b
The theorem `ENNReal.lt_add_right` states that for all extended nonnegative real numbers `a` and `b`, if `a` is not equal to positive infinity and `b` is not zero, then `a` is less than the sum of `a` and `b`. This is a formalization of the common mathematical property that a real number is always less than the sum of itself and a positive number.
More concisely: For all extended nonnegative real numbers `a` and `b` not equal to positive infinity with `b` nonzero, `a < a + b`.
|
ENNReal.mul_le_mul_left
theorem ENNReal.mul_le_mul_left : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → (a * b ≤ a * c ↔ b ≤ c)
This theorem states that for all extended nonnegative real numbers 'a', 'b', and 'c', if 'a' is neither zero nor positive infinity, then the product of 'a' and 'b' being less than or equal to the product of 'a' and 'c' implies that 'b' is less than or equal to 'c'. In essence, it validates that multiplication by a positive non-infinite factor does not affect the order relationship between 'b' and 'c'.
More concisely: If 'a' is a finite non-negative real number and 'a' * 'b' <= 'a' * 'c', then 'b' <= 'c'.
|
ENNReal.cancel_coe
theorem ENNReal.cancel_coe : ∀ {a : NNReal}, AddLECancellable ↑a
The theorem `ENNReal.cancel_coe` asserts that for every nonnegative real number `a`, the function `x ↦ a + x` is order-reflecting. This characteristic is described by the property `AddLECancellable` in the Lean 4 library. In other words, if you have two elements `b` and `c` such that `a + b` is less than or equal to `a + c`, then `b` is also less than or equal to `c`. The addition of `a` can be "cancelled" in an inequality comparison, hence the term `cancel_coe`.
More concisely: For every non-negative real number `a`, the function `x ↦ a + x` is order-preserving, i.e., if `b ≤ c`, then `a + b ≤ a + c`.
|
ENNReal.sub_top
theorem ENNReal.sub_top : ∀ {a : ENNReal}, a - ⊤ = 0
This theorem states that for any extended nonnegative real number 'a', the difference between 'a' and infinity (denoted as '⊤') is always zero. It's a special case of the theorem `WithTop.sub_top` in the extended nonnegative real numbers (`ENNReal`) namespace. This theorem is crucial in the analysis involving measures, where extended nonnegative real numbers are often used to represent the sizes of sets that could potentially be infinite.
More concisely: For any extended nonnegative real number 'a', a - ⊤ = 0.
|
ENNReal.add_ne_top
theorem ENNReal.add_ne_top : ∀ {a b : ENNReal}, a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
The theorem `ENNReal.add_ne_top` states that for any two extended nonnegative real numbers `a` and `b`, the sum of `a` and `b` is not equal to positive infinity if and only if neither `a` nor `b` are equal to positive infinity. In other words, positive infinity can only be resulted from the sum if at least one of the summands is positive infinity.
More concisely: For extended nonnegative real numbers `a` and `b`, the sum `a + b` is not positive infinity if and only if neither `a` nor `b` are positive infinity.
|
ENNReal.sum_lt_top
theorem ENNReal.sum_lt_top :
∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, (∀ a ∈ s, f a ≠ ⊤) → (s.sum fun a => f a) < ⊤
This theorem states that the sum of a finite number of extended nonnegative real numbers is still a finite number. More specifically, given a finite set `s` and a function `f` mapping elements of `s` to extended nonnegative real numbers (denoted as [0, ∞]), if every element `a` in `s` under the function `f` does not map to ∞ (the symbol for infinity), then the sum of `f(a)` over all `a` in `s` is less than ∞. In other words, it's impossible for a sum of finitely many non-infinite extended nonnegative real numbers to result in infinity.
More concisely: Given a finite set and a function mapping each element to a finite extended nonnegative real number, the sum of the function values is also a finite extended nonnegative real number.
|
ENNReal.cancel_of_lt
theorem ENNReal.cancel_of_lt : ∀ {a : ENNReal}, a < ⊤ → AddLECancellable a
This theorem, called `ENNReal.cancel_of_lt`, states that for any element `a` of the extended nonnegative real numbers (`ENNReal`), if `a` is less than infinity (denoted by `⊤`), then `a` has the property of being `AddLECancellable`. This means that for any two other elements `b` and `c` of the same type, if `a + b` is less than or equal to `a + c`, then `b` is less than or equal to `c`. In other words, the addition of `a` does not affect the order of `b` and `c`. This property is frequently used in the context of `ENNReal`, hence the abbreviated name of the theorem.
More concisely: For any `a` in `ENNReal` with `a < ⊤`, `a` is `AddLECancellable`, meaning `a + b <= a + c` implies `b <= c`.
|
ENNReal.mul_left_strictMono
theorem ENNReal.mul_left_strictMono : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → StrictMono fun x => a * x
The theorem `ENNReal.mul_left_strictMono` states that for any extended nonnegative real number `a` which is neither zero nor positive infinity, the function that multiplies `a` to its input is strictly monotonic. In other words, for any two distinct inputs, the one that is larger will have a larger output after multiplication by `a`. This corresponds to the mathematical statement that multiplication by a positive real number preserves the order of real numbers.
More concisely: For any extended non-zero non-positive infinity real number `a`, the function `x => a * x` is strictly increasing on the set of real numbers.
|
ENNReal.sum_lt_top_iff
theorem ENNReal.sum_lt_top_iff :
∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, (s.sum fun a => f a) < ⊤ ↔ ∀ a ∈ s, f a < ⊤
This theorem states that the sum of a set of finite extended nonnegative real numbers is also finite. More precisely, for any type `α`, any finite set `s` of `α`, and any function `f` from `α` to extended nonnegative real numbers, the sum of the function `f` applied to each element of `s` is less than infinity if and only if each element `a` in `s` returns a finite value when applied to the function `f`.
More concisely: For any type `α`, a finite set `s` of `α`, and a function `f` from `α` to extended nonnegative real numbers, the sum of `f` over `s` is finite if and only if all elements in `s` have finite values under `f`.
|
ENNReal.pow_pos
theorem ENNReal.pow_pos : ∀ {a : ENNReal}, 0 < a → ∀ (n : ℕ), 0 < a ^ n
This theorem states that for all extended nonnegative real numbers `a`, if `a` is greater than zero, then for any natural number `n`, `a` raised to the power `n` is also greater than zero. In other words, the power of any positive extended nonnegative real number is also positive.
More concisely: For all extended nonnegative real numbers `a` greater than zero, `a^n` is positive for any natural number `n`.
|
ENNReal.prod_lt_top
theorem ENNReal.prod_lt_top :
∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, (∀ a ∈ s, f a ≠ ⊤) → (s.prod fun a => f a) < ⊤
This theorem states that the product of a finite set of extended nonnegative real numbers is still finite. More formally, given any type `α`, a finite set `s` of `α`, and a function `f` mapping elements of `α` to extended nonnegative real numbers (`ENNReal`), if for all elements `a` in `s`, `f(a)` is not equal to infinity (`⊤`), then the product of `f(a)` for all `a` in `s` is also less than infinity.
More concisely: If `f` is a function mapping a finite set `s` of real numbers to extended nonnegative real numbers such that `f(a)` is finite for all `a` in `s`, then the product of `f(a)` for all `a` in `s` is finite.
|
ENNReal.cancel_of_ne
theorem ENNReal.cancel_of_ne : ∀ {a : ENNReal}, a ≠ ⊤ → AddLECancellable a
This theorem, named `ENNReal.cancel_of_ne`, states that for any element `a` in the extended nonnegative real numbers (usually denoted as [0, ∞]), if `a` is not equal to infinity, then `a` possesses the property of being `AddLECancellable`. In other words, the function `x ↦ a + x` is order-reflecting for such `a`. This implies that for all `b` and `c` in the same set, if `a + b` is less than or equal to `a + c`, then `b` itself is less than or equal to `c`.
More concisely: For any finite element `a` in the extended nonnegative real numbers, the function `x mapsto a + x` is order-reflecting.
|
ENNReal.sum_eq_top_iff
theorem ENNReal.sum_eq_top_iff :
∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal}, (s.sum fun x => f x) = ⊤ ↔ ∃ a ∈ s, f a = ⊤
This theorem states that a sum of numbers, specifically extended nonnegative real numbers, is infinite if and only if at least one of the elements in the set being summed is infinite. The function 'f' maps elements of an arbitrary type 'α' to extended nonnegative real numbers, and 's' is a finite set of elements of this type. 's' is being summed over with this function. So, in mathematical terms, over a set 's' and a function 'f' from 's' to extended nonnegative real numbers, this theorem asserts that the sum over 's' of 'f(x)', denoted as $\sum_{x\in s}f(x)$, equals infinity if and only if there exists an element 'a' in 's' such that 'f(a)' equals infinity.
More concisely: A sum of extended nonnegative real numbers over a finite set is infinite if and only if one of the numbers in the sum is infinite.
|
Mathlib.Data.ENNReal.Operations._auxLemma.6
theorem Mathlib.Data.ENNReal.Operations._auxLemma.6 :
∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, (a < ⊤) = (a ≠ ⊤)
This theorem states that for any type `α` that has a partial order and a greatest element (`⊤`), the inequality `a < ⊤` is equivalent to the inequality `a ≠ ⊤` for any element `a` of type `α`. In other words, any element of such a type that is not equal to the greatest element is necessarily less than the greatest element.
More concisely: For any type with a greatest element under a partial order, the inequality `a < ⊤` is equivalent to `a ≠ ⊤` for all `a` in the type.
|
ENNReal.toReal_sum
theorem ENNReal.toReal_sum :
∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal},
(∀ a ∈ s, f a ≠ ⊤) → (s.sum fun a => f a).toReal = s.sum fun a => (f a).toReal
This theorem states that for any finite set `s` of elements of type `α` and any function `f` from `α` to the extended nonnegative real numbers (usually denoted [0, ∞]), if no element in `s` is mapped to infinity by `f`, then the sum of the images of the elements of `s` under `f` (interpreted as real numbers) is equal to the real number corresponding to the sum of the images of the elements of `s` under `f` (interpreted as extended nonnegative real numbers). In other words, viewing extended nonnegative real numbers as real numbers does not alter the sum of a set of such numbers, provided none of them are infinity.
More concisely: For any finite set `s` of real numbers and function `f` from real numbers to [0, ∞] such that `f(x)` is finite for all `x` in `s`, the sum of the images of `s` under `f` as real numbers equals the sum of the images of `s` under `f` as extended nonnegative real numbers.
|
ENNReal.top_pow
theorem ENNReal.top_pow : ∀ {n : ℕ}, 0 < n → ⊤ ^ n = ⊤
This theorem states that for any positive natural number `n`, the `n`th power of positive infinity (`⊤`) is also positive infinity. In other words, raising positive infinity to any positive natural number exponent does not change its value, it remains positive infinity. This is consistent with the general understanding of infinity in mathematics.
More concisely: For any positive natural number `n`, `⊤^n = ⊤`.
|
ENNReal.mul_right_mono
theorem ENNReal.mul_right_mono : ∀ {a : ENNReal}, Monotone fun x => x * a
The theorem `ENNReal.mul_right_mono` states that for every extended nonnegative real number `a`, the multiplication function `fun x => x * a` is monotone. In other words, if we have two extended nonnegative real numbers where the first is less than or equal to the second, then the result of multiplying the first number by `a` will be less than or equal to the result of multiplying the second number by `a`. This is the property of right multiplication being monotone in the extended nonnegative real numbers.
More concisely: For all extended nonnegative real numbers `a` and `x` with `x_1 ≤ x_2`, we have `x_1 * a ≤ x_2 * a`.
|
ENNReal.mul_top
theorem ENNReal.mul_top : ∀ {a : ENNReal}, a ≠ 0 → a * ⊤ = ⊤
This theorem states that for any extended nonnegative real number `a` that is not equal to zero, the product of `a` and positive infinity (denoted as `⊤`) equals positive infinity. In other words, multiplying any nonzero extended nonnegative real number by positive infinity results in positive infinity.
More concisely: For any nonzero extended nonnegative real number `a`, `a * ⊤ = ⊤`.
|
ENNReal.mul_lt_top
theorem ENNReal.mul_lt_top : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → a * b < ⊤
The theorem `ENNReal.mul_lt_top` states that for all extended nonnegative real numbers `a` and `b`, if neither `a` nor `b` is equal to positive infinity (denoted by `⊤`), then the product of `a` and `b` is strictly less than positive infinity. This is relevant in the context of measures, where the codomain of a measure is the set of extended nonnegative real numbers, which includes positive infinity. Hence, this theorem guarantees that as long as neither of the factors is infinity, the product will also not be infinity.
More concisely: For all extended nonnegative real numbers `a` and `b` not equal to positive infinity, `a * b < ⊤`.
|
ENNReal.coe_sub
theorem ENNReal.coe_sub : ∀ {r p : NNReal}, ↑(r - p) = ↑r - ↑p
This theorem, `ENNReal.coe_sub`, states that for any two nonnegative real numbers `r` and `p`, the result of subtracting `p` from `r` and then taking the "coercion" of that result (essentially, thinking of the result as an extended nonnegative real number) is the same as taking the "coercion" of `r` and `p` separately and then subtracting these. This is a special case of the more general theorem `WithTop.coe_sub` in the context of extended nonnegative real numbers.
More concisely: For any nonnegative real numbers `r` and `p`, the coercion of `r - p` is equivalent to the coercion of `r` followed by the coercion of `-p`.
|
ENNReal.smul_def
theorem ENNReal.smul_def : ∀ {M : Type u_1} [inst : MulAction ENNReal M] (c : NNReal) (x : M), c • x = ↑c • x := by
sorry
This theorem states that for any type `M` with a multiplication action defined on it by the extended nonnegative real numbers (`ENNReal`), and given a nonnegative real number (`NNReal`) `c` and an element `x` of type `M`, the scalar multiplication operation `c • x` is equivalent to the scalar multiplication of the coerced value of `c` to `ENNReal` and `x`, written as `↑c • x`. In simpler terms, it shows that for any nonnegative real number and an element of a particular type, you can perform scalar multiplication as though the nonnegative real number was an extended nonnegative real number.
More concisely: For any type `M` with multiplication action by nonnegative real numbers, and for any nonnegative real number `c` and element `x` of `M`, `c • x` is equal to `↑c • x`, where `↑c` is the coerced value of `c` to `ENNReal`.
|
ENNReal.eq_sub_of_add_eq
theorem ENNReal.eq_sub_of_add_eq : ∀ {a b c : ENNReal}, c ≠ ⊤ → a + c = b → a = b - c
This theorem states that for every three extended nonnegative real numbers `a`, `b`, and `c`, where `c` is not positive infinity (`⊤`), if `a` added to `c` equals `b`, then `a` is equal to `b` subtracted by `c`. In other words, if `a + c = b`, then `a = b - c`. This theorem constitutes a fundamental property of addition and subtraction in the space of extended nonnegative real numbers.
More concisely: For all extended nonnegative real numbers `a`, `b`, and `c` (`c ≠ ⊤`), if `a + c = b`, then `a = b - c`.
|
ENNReal.add_lt_add
theorem ENNReal.add_lt_add : ∀ {a b c d : ENNReal}, a < c → b < d → a + b < c + d
This theorem states that for any four extended nonnegative real numbers (commonly denoted as [0, ∞]), if the first is less than the third and the second is less than the fourth, then the sum of the first and second is less than the sum of the third and fourth. In other words, for all `a`, `b`, `c`, `d` in the set of extended nonnegative real numbers, if `a < c` and `b < d`, then `a + b < c + d`.
More concisely: For all extended nonnegative real numbers `a`, `b`, `c`, `d`, if `a < c` and `b < d`, then `a + b < c + d`.
|
ENNReal.sub_mul
theorem ENNReal.sub_mul : ∀ {a b c : ENNReal}, (0 < b → b < a → c ≠ ⊤) → (a - b) * c = a * c - b * c
This theorem states that for any three extended nonnegative real numbers `a`, `b`, and `c`, given that `b` is positive and less than `a`, and `c` is not infinity, the multiplication of the difference between `a` and `b` with `c` is equal to the difference of the product of `a` and `c` and the product of `b` and `c`. In mathematical terms, it asserts that if `0 < b < a` and `c ≠ ∞`, then `(a - b) * c = a * c - b * c`. This is akin to the property of distributivity of multiplication over subtraction, extended to include nonnegative real numbers and infinity.
More concisely: For non-negative real numbers `a`, `b`, and `c` with `0 < b < a` and `c neq ∞`, we have `(a - b) * c = a * c - b * c`.
|
ENNReal.sub_lt_self
theorem ENNReal.sub_lt_self : ∀ {a b : ENNReal}, a ≠ ⊤ → a ≠ 0 → b ≠ 0 → a - b < a
This theorem states that for any two extended nonnegative real numbers 'a' and 'b', where 'a' is not infinite (denoted by ⊤) and both 'a' and 'b' are not zero, the difference of 'a' and 'b' is less than 'a'. In other words, subtracting a positive value from an extended nonnegative real number (that is not infinite) always results in a lesser value.
More concisely: For any extended nonnegative real numbers 'a' and 'b' with 'a' finite and 'b' nonzero, we have a < a + b.
|
ENNReal.mul_eq_top
theorem ENNReal.mul_eq_top : ∀ {a b : ENNReal}, a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
The theorem `ENNReal.mul_eq_top` states that for all elements `a` and `b` of the set of extended nonnegative real numbers (`ENNReal`), the product `a * b` equals infinity (`⊤`) if and only if either `a` is not equal to zero and `b` equals infinity, or `a` equals infinity and `b` is not equal to zero. This theorem thus characterizes the conditions under which multiplication in the extended nonnegative real numbers results in infinity.
More concisely: The extended nonnegative real numbers `a * b = ⊤` if and only if `a ≠ 0 ∧ b = ⊤` or `a = ⊤ ∧ b ≠ 0`.
|
ENNReal.mul_left_mono
theorem ENNReal.mul_left_mono : ∀ {a : ENNReal}, Monotone fun x => a * x
The theorem `ENNReal.mul_left_mono` states that for any extended nonnegative real number `a`, the function that multiplies `a` with a variable `x` is monotone. In other words, if `x` and `y` are two extended nonnegative real numbers such that `x ≤ y`, then `a * x ≤ a * y`. This property holds regardless of the specific value of `a`.
More concisely: For all extended nonnegative real numbers `a` and `x` with `x <= y`, we have `a * x <= a * y`.
|
ENNReal.add_lt_top
theorem ENNReal.add_lt_top : ∀ {a b : ENNReal}, a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤
This theorem states that for all pairs of extended nonnegative real numbers 'a' and 'b', the sum of 'a' and 'b' is less than infinity if and only if both 'a' and 'b' are each less than infinity. In other words, in the context of extended nonnegative real numbers, if the sum of two numbers is finite, then those two numbers must themselves be finite.
More concisely: For all extended nonnegative real numbers 'a' and 'b', the sum 'a' + 'b' is finite if and only if both 'a' and 'b' are finite.
|
ENNReal.mul_pos
theorem ENNReal.mul_pos : ∀ {a b : ENNReal}, a ≠ 0 → b ≠ 0 → 0 < a * b
This theorem states that for any two extended nonnegative real numbers `a` and `b`, if neither `a` nor `b` is equal to zero, then the product of `a` and `b` is greater than zero. In other words, the multiplication of any two nonzero extended nonnegative real numbers always results in a positive number. This is consistent with the property of real numbers where the product of two positive numbers is always positive.
More concisely: For any two nonzero extended nonnegative real numbers `a` and `b`, their product is positive.
|
ENNReal.mul_lt_top_iff
theorem ENNReal.mul_lt_top_iff : ∀ {a b : ENNReal}, a * b < ⊤ ↔ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
The theorem `ENNReal.mul_lt_top_iff` states that for any two extended nonnegative real numbers `a` and `b`, the product `a * b` is less than infinity if and only if either both `a` and `b` are less than infinity, or `a` is zero, or `b` is zero. In other words, you can only ensure that the multiplication of `a` and `b` won't result in infinity if both `a` and `b` are finite or one of them is zero.
More concisely: For extended nonnegative real numbers `a` and `b`, `a * b` is less than infinity if and only if both `a` and `b` are finite or one of them is zero.
|
ENNReal.top_mul'
theorem ENNReal.top_mul' : ∀ {a : ENNReal}, ⊤ * a = if a = 0 then 0 else ⊤
The theorem `ENNReal.top_mul'` states that for any extended nonnegative real number 'a', the multiplication of '⊤' (which represents infinity) and 'a' is equal to '⊤' if 'a' is not zero. If 'a' is zero, then the result of the multiplication is zero. This mirrors the conventional mathematical understanding that multiplying infinity by any non-zero number results in infinity, and multiplying infinity by zero results in zero.
More concisely: For any extended non-negative real number 'a', '⊤ * a = ⊤' if 'a' is non-zero, and '⊤ * 0 = 0'.
|
ENNReal.mul_ne_top
theorem ENNReal.mul_ne_top : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → a * b ≠ ⊤
This theorem states that for any two extended non-negative real numbers `a` and `b`, if neither `a` nor `b` are infinity (notated as `⊤`), then the product of `a` and `b` also cannot be infinity. In other words, the multiplication of two finite extended non-negative real numbers results in a finite number, not infinity.
More concisely: For any extended non-negative real numbers `a` and `b` not equal to infinity, their product is a finite real number.
|
ENNReal.addLECancellable_iff_ne
theorem ENNReal.addLECancellable_iff_ne : ∀ {a : ENNReal}, AddLECancellable a ↔ a ≠ ⊤
This theorem states that for an element `a` in the set of extended nonnegative real numbers (usually denoted as [0, ∞]), `a` is `AddLECancellable` (meaning that if `a + b ≤ a + c`, then `b ≤ c` for all `b` and `c`) if and only if `a` is not equal to infinity. In other words, all elements in the extended nonnegative real numbers, except infinity, have the property that adding them to another number and comparing the sums can reflect the order of the original numbers.
More concisely: An element in the extended nonnegative real numbers is AddLECancellable if and only if it is finite.
|
ENNReal.top_mul
theorem ENNReal.top_mul : ∀ {a : ENNReal}, a ≠ 0 → ⊤ * a = ⊤
This theorem states that for all values `a` of the type `ENNReal` (which represents the extended nonnegative real numbers, usually denoted as [0, ∞]), if `a` is not equal to 0, then the multiplication of the special value `⊤` (which represents infinity in this context) and `a` equals `⊤`. This essentially mirrors the mathematical concept that multiplying any non-zero real number with infinity yields infinity.
More concisely: For all `a` in `ENNReal`, `a *= ⊤` equals `⊤` if `a` is non-zero.
|
ENNReal.mul_top'
theorem ENNReal.mul_top' : ∀ {a : ENNReal}, a * ⊤ = if a = 0 then 0 else ⊤
The theorem `ENNReal.mul_top'` states that for every element `a` of the extended nonnegative real numbers (ENNReal), the product of `a` and positive infinity (`⊤`) is determined by whether `a` is zero. If `a` is zero, then the product is zero. Otherwise, if `a` is nonzero, then the product is positive infinity (`⊤`).
More concisely: For every `a` in ENNReal, `a * ⊤ = ⊤` if `a` is nonzero, and `a * ⊤ = 0` if `a` is zero.
|