Mathlib.Data.ENNReal.Basic._auxLemma.1
theorem Mathlib.Data.ENNReal.Basic._auxLemma.1 : ∀ {p q : NNReal}, (↑p = ↑q) = (p = q)
This theorem states that for all nonnegative real numbers `p` and `q` (denoted by `NNReal`), the equality of their embeddings into another type (denoted by `↑p` and `↑q`) is equivalent to their direct equality. In other words, if the embedded forms of two nonnegative real numbers are equal, then the original nonnegative real numbers themselves are equal, and vice versa.
More concisely: For all nonnegative real numbers `p` and `q`, `↑p = ↑q` if and only if `p = q`.
|
ENNReal.iUnion_Iio_coe_nat
theorem ENNReal.iUnion_Iio_coe_nat : ⋃ n, Set.Iio ↑n = {⊤}ᶜ
This theorem states that the union of left-infinite right-open intervals for all natural numbers, where each interval is defined as the set of all extended non-negative real numbers less than the corresponding natural number, is equal to the complement of the set containing only the element `⊤` (which represents infinity in the context of extended non-negative real numbers). In other words, every extended non-negative real number that is not infinity is less than some natural number.
More concisely: The set of all extended non-negative real numbers less than every natural number forms a set equal to the complement of {⊤} in the extended non-negative real numbers.
|
ENNReal.coe_le_coe
theorem ENNReal.coe_le_coe : ∀ {r q : NNReal}, ↑r ≤ ↑q ↔ r ≤ q
This theorem states that for all nonnegative real numbers `r` and `q`, the coercion of `r` to extended nonnegative real numbers is less than or equal to the coercion of `q` to extended nonnegative real numbers if and only if `r` is less than or equal to `q`. In mathematical terms, it's establishing that the order of `r` and `q` is preserved when they are embedded into the space of extended nonnegative real numbers.
More concisely: For all nonnegative real numbers `r` and `q`, `r ≤ q` if and only if the coercion of `r` to extended nonnegative real numbers is less than or equal to the coercion of `q` to extended nonnegative real numbers.
|
ENNReal.le_inv_smul_iff_of_pos
theorem ENNReal.le_inv_smul_iff_of_pos :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α]
[inst_2 : Preorder β] [inst_3 : MulAction α β] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β],
0 < a → (b₁ ≤ a⁻¹ • b₂ ↔ a • b₁ ≤ b₂)
This theorem, "ENNReal.le_inv_smul_iff_of_pos", states that for any types `α` and `β`, with `α` being a group with zero and `β` being an ordered type, and given any instances of `α` and `β` being a multiplicative action and satisfying the positive scalar multiplication monotone and reflection laws, if `a` is a positive element of `α`, then `b₁` is less than or equal to the inverse of `a` multiplied by `b₂` if and only if `a` multiplied by `b₁` is less than or equal to `b₂`.
More concisely: For any group with zero `α` and ordered type `β`, if `a` is a positive element of `α`, then `b₁ ≤ a⁻¹ * b₂` if and only if `a * b₁ ≤ b₂`.
|
ENNReal.one_toReal
theorem ENNReal.one_toReal : 1.toReal = 1
This theorem states that the real number representation of 1, as obtained by the 'toReal' function, is equal to 1. In other words, when the integer 1 is converted to a real number using the 'toReal' function, it remains 1.
More concisely: The theorem asserts that the real number representation of the integer 1, obtained through the 'toReal' function, is equal to 1. (or) The 'toReal' function applied to the integer 1 results in the real number 1.
|
ENNReal.ofReal_coe_nat
theorem ENNReal.ofReal_coe_nat : ∀ (n : ℕ), ENNReal.ofReal ↑n = ↑n
This theorem states that for any natural number 'n', the function 'ENNReal.ofReal' applied to the real number representation of 'n' is equal to the co-domain representation of 'n'. In simpler terms, when you convert a natural number to a real number and apply the 'ENNReal.ofReal' function, it behaves the same as if you directly converted the natural number to the co-domain.
More concisely: For any natural number n, ENNReal.ofReal (realNumberRepresentationOf n) = coDomainRepresentationOf n.
|
ENNReal.top_ne_zero
theorem ENNReal.top_ne_zero : ⊤ ≠ 0
This theorem states that in the extended non-negative real number system (ENNReal), the positive infinity symbol, represented as "⊤", is not equal to zero. In other words, in this system, positive infinity and zero are distinct entities and cannot be equivalent.
More concisely: In the extended non-negative real number system (ENNReal), 0 and ∞ (positive infinity) are distinct.
|
ENNReal.toNNReal_coe
theorem ENNReal.toNNReal_coe : ∀ {r : NNReal}, (↑r).toNNReal = r
The theorem `ENNReal.toNNReal_coe` states that for any nonnegative real number `r` (represented by `NNReal`), when `r` is explicitly cast (using `↑` operation) to an extended nonnegative real number and then mapped back to a nonnegative real number using `.toNNReal` operation, it remains the same `r`. In other words, the process of casting a nonnegative real number to an extended nonnegative real number and then back to a nonnegative real number is identity-preserving, confirming the consistency between these two types.
More concisely: For any non-negative real number `r`, the conversion `↑r`.toNNReal equals `r`.
|
ENNReal.coe_mul
theorem ENNReal.coe_mul : ∀ (x y : NNReal), ↑(x * y) = ↑x * ↑y
This theorem states that for any two nonnegative real numbers `x` and `y`, the operation of taking their product in the nonnegative real numbers (`x * y`) and then taking its real part (denoted by `↑(x * y)`) is the same as first taking their real parts (`↑x` and `↑y`) and then multiplying these real numbers. In other words, multiplication in the nonnegative real numbers commutes with the operation of taking the real part.
More concisely: For all non-negative real numbers x and y, ↑(x * y) = ↑x * ↑y.
|
ENNReal.top_toReal
theorem ENNReal.top_toReal : ⊤.toReal = 0
This theorem states that the real-number representation (`toReal`) of "top" (`⊤`), in the extended non-negative real number system (`ENNReal`), is equal to zero. In the context of `ENNReal`, "top" typically represents an element that is greater than any ordinary (non-top) element in the set, which is typically seen as positive infinity. However, when this "top" is converted to real numbers, it equals zero according to this theorem.
More concisely: The theorem asserts that the conversion of the top element in the extended non-negative real number system to real numbers equals zero. (or more concisely: The top element in the extended non-negative real number system maps to zero when converted to real numbers.)
|
ENNReal.coe_mono
theorem ENNReal.coe_mono : Monotone ENNReal.ofNNReal
The theorem `ENNReal.coe_mono` states that the function `ENNReal.ofNNReal`, which is a coercion from nonnegative real numbers (`ℝ≥0` or `NNReal` in Lean 4) to extended nonnegative real numbers (`ℝ≥0∞` or `ENNReal` in Lean 4), is a monotone function. In mathematical terms, if `a` and `b` are nonnegative real numbers and `a ≤ b`, then `ENNReal.ofNNReal a ≤ ENNReal.ofNNReal b`. This means that the extended nonnegative real number corresponding to `a` is less than or equal to the extended nonnegative real number corresponding to `b`.
More concisely: The coercion `ENNReal.ofNNReal` from nonnegative real numbers to extended nonnegative real numbers is a monotone function.
|
ENNReal.coe_nat
theorem ENNReal.coe_nat : ∀ (n : ℕ), ↑↑n = ↑n
This theorem states that for any natural number `n`, the process of first casting `n` to a non-negative real number (`ENNReal`), and then casting the result to a real number results in the same value as directly casting `n` to a real number. In other words, the two-step casting process doesn't change the value of `n` in any way when compared to direct casting. This is represented symbolically by the equality `↑↑n = ↑n`.
More concisely: For all natural numbers `n`, the double casting from `Nat` to `Real` (`↑↑n`) is equal to the direct casting from `Nat` to `Real` (`↑n`).
|
ENNReal.toReal_nonneg
theorem ENNReal.toReal_nonneg : ∀ {a : ENNReal}, 0 ≤ a.toReal
This theorem states that for any element `a` of the type `ENNReal` (which represents the extended nonnegative real numbers, including positive infinity), the real number representation of `a` is always nonnegative. Or in other words, the conversion of any extended nonnegative real number to a real number will always result in a number that is greater than or equal to zero. This makes sense because `ENNReal` is defined to only contain nonnegative numbers (ranging from zero to positive infinity).
More concisely: For any `a` in `ENNReal`, the real number representation of `a` is nonnegative.
|
ENNReal.coe_inj
theorem ENNReal.coe_inj : ∀ {p q : NNReal}, ↑p = ↑q ↔ p = q
This theorem, named `ENNReal.coe_inj`, states that for any two nonnegative real numbers `p` and `q`, the equality of their coercions (i.e., their representations as extended nonnegative real numbers) implies the equality of `p` and `q` themselves. In other words, the process of coercion preserves equality in the set of nonnegative real numbers.
More concisely: For all non-negative real numbers p and q, if p = q as extended real numbers then p = q.
|
ENNReal.nat_ne_top
theorem ENNReal.nat_ne_top : ∀ (n : ℕ), ↑n ≠ ⊤
This theorem states that, for any natural number `n`, the real number equivalent of `n` is not equal to infinity. In other words, the real number representation of any natural number will never be infinity.
More concisely: For all natural numbers `n`, the real number representation `n` is finite.
|
ENNReal.coe_add
theorem ENNReal.coe_add : ∀ (x y : NNReal), ↑(x + y) = ↑x + ↑y
This theorem states that for any two nonnegative real numbers 'x' and 'y', the operation of taking the sum (x + y) and then applying the coercion function (↑) is the same as first applying the coercion to 'x' and 'y' separately and then taking the sum of the results. In other words, the coercion function preserves the operation of addition on nonnegative real numbers.
More concisely: For any nonnegative real numbers x and y, ↑(x + y) = ↑x + ↑y.
|
Mathlib.Data.ENNReal.Basic._auxLemma.20
theorem Mathlib.Data.ENNReal.Basic._auxLemma.20 : ∀ {r q : NNReal}, (↑r < ↑q) = (r < q)
The theorem `Mathlib.Data.ENNReal.Basic._auxLemma.20` states that for any two nonnegative real numbers `r` and `q`, the inequality of their real number counterparts (`↑r < ↑q`) is equivalent to the inequality of the original nonnegative real numbers (`r < q`). In other words, the process of converting nonnegative real numbers to real numbers preserves the order of inequality.
More concisely: For any nonnegative real numbers r and q, the inequality r < q is equivalent to the inequality ↑r < ↑q, where ↑ is the function that lifts nonnegative real numbers to real numbers.
|
ENNReal.zero_ne_top
theorem ENNReal.zero_ne_top : 0 ≠ ⊤
This theorem states that zero is not equal to positive infinity in the context of extended non-negative real numbers. In other words, in the numerical system that includes positive infinity as a value, zero is distinctly different from this infinite value.
More concisely: Zero is not equal to positive infinity in the extended non-negative real numbers.
|
ENNReal.iUnion_Iic_coe_nat
theorem ENNReal.iUnion_Iic_coe_nat : ⋃ n, Set.Iic ↑n = {⊤}ᶜ
This theorem states that the union over all natural numbers `n` of the sets of extended non-negative real numbers less than or equal to `n` (the union of left-infinite right-closed intervals) is equal to the set of all extended non-negative real numbers excluding positive infinity (`{⊤}ᶜ`). In other words, it asserts that every non-infinite extended non-negative real number is less than or equal to some natural number.
More concisely: The set of all extended non-negative real numbers less than or equal to the union of the left-infinite right-closed intervals over all natural numbers is equal to the set of all finite extended non-negative real numbers, excluding positive infinity.
|
ENNReal.ofReal_toReal
theorem ENNReal.ofReal_toReal : ∀ {a : ENNReal}, a ≠ ⊤ → ENNReal.ofReal a.toReal = a
This theorem states that for every extended nonnegative real number `a` that is not equal to positive infinity, the function `ENNReal.ofReal` applied to the real part of `a` (obtained by `a.toReal`) is equal to `a` itself. In simple terms, this means that if we convert a non-infinite extended nonnegative real number to a real number and then back to an extended nonnegative real number, we get the original number back. This implies the "consistency" between the conversion functions `toReal` and `ofReal` in the context of extended nonnegative real numbers.
More concisely: For every finite extended non-negative real number `a`, `ENNReal.ofReal (a.toReal) = a`.
|
ENNReal.ofReal_eq_coe_nnreal
theorem ENNReal.ofReal_eq_coe_nnreal : ∀ {x : ℝ} (h : 0 ≤ x), ENNReal.ofReal x = ↑⟨x, h⟩
The theorem `ENNReal.ofReal_eq_coe_nnreal` states that for any real number `x` that is nonnegative (i.e., `0 ≤ x`), the function `ENNReal.ofReal` applied to `x` is equal to the coercion of the nonnegative real number represented by `x` and its nonnegativity property. In other words, for any nonnegative real number `x`, the operation of "turning a real number into a nonnegative extended real number" performed by `ENNReal.ofReal` is equivalent to directly constructing a nonnegative real number with value `x` and proving its nonnegativity.
More concisely: For any non-negative real number `x`, `ENNReal.ofReal x = ⟦x, 0 ≤ x⟧`.
|
ENNReal.one_lt_top
theorem ENNReal.one_lt_top : 1 < ⊤
This theorem, `ENNReal.one_lt_top`, states that one is less than infinity in the context of extended non-negative real numbers. In mathematical notation, this theorem is asserting that 1 < ∞. This is commonly accepted in mathematics as infinity is considered greater than any real number.
More concisely: One is strictly less than infinity in the extended non-negative real numbers.
|
ENNReal.one_ne_top
theorem ENNReal.one_ne_top : 1 ≠ ⊤
This theorem states that the number 1 is not equal to positive infinity (`⊤`) in the extended non-negative real numbers (`ENNReal`). In other words, in the context of the extended non-negative real number system, the real number 1 and positive infinity are distinct entities.
More concisely: The theorem asserts that 1 and Positive Infinity (⊤) in the extended non-negative real numbers (ENNReal) are distinct.
|
ENNReal.ofReal_lt_top
theorem ENNReal.ofReal_lt_top : ∀ {r : ℝ}, ENNReal.ofReal r < ⊤
The theorem `ENNReal.ofReal_lt_top` states that for any real number `r`, the `ENNReal.ofReal r` function always gives a result that is less than infinity. In other words, the function `ENNReal.ofReal` maps any real number to a nonnegative extended real number (including zero), but never to infinity. Therefore, the image of this function does not include the "positive infinity" value.
More concisely: For all real numbers r, the image of `ENNReal.ofReal r` is a non-positive extended real number.
|
ENNReal.ofReal_one
theorem ENNReal.ofReal_one : ENNReal.ofReal 1 = 1
The theorem `ENNReal.ofReal_one` states that if we apply the function `ENNReal.ofReal` to the real number `1`, the result is `1`. This makes sense since `1` is nonnegative, so `ENNReal.ofReal` just returns the same value `1`.
More concisely: The theorem `ENNReal.ofReal_one` asserts that `ENNReal.ofReal 1 = 1`.
|
ENNReal.toReal_ofNat
theorem ENNReal.toReal_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).toReal = OfNat.ofNat n
The theorem `ENNReal.toReal_ofNat` states that for all natural numbers `n` that are at least two, the real number representation of `n` obtained using the `toReal` function on the `OfNat.ofNat n` object equals the `OfNat.ofNat n` object itself. In other words, for natural numbers that are at least two, converting them to `OfNat` objects and then to real numbers will not change their identity.
More concisely: For all natural numbers `n` greater than or equal to 2, `OfNat.ofNat n = toReal (OfNat.ofNat n)`.
|
ENNReal.coe_ne_zero
theorem ENNReal.coe_ne_zero : ∀ {r : NNReal}, ↑r ≠ 0 ↔ r ≠ 0
This theorem is stating that for any nonnegative real number `r`, the coercion of `r` to an extended nonnegative real number (indicated by `↑r`) is not equal to zero if and only if `r` is not equal to zero. This means that zero in the context of nonnegative real numbers and extended nonnegative real numbers is consistent; a nonnegative real number is zero if and only if its corresponding extended nonnegative real number is zero.
More concisely: For any nonnegative real number `r`, `↑r = 0` if and only if `r = 0`.
|
Mathlib.Data.ENNReal.Basic._auxLemma.25
theorem Mathlib.Data.ENNReal.Basic._auxLemma.25 : ∀ {r : NNReal}, (0 < ↑r) = (0 < r)
The theorem `Mathlib.Data.ENNReal.Basic._auxLemma.25` states that for all nonnegative real numbers `r` (represented by `NNReal`), the proposition that the real part of `r` (obtained by coercion `↑r`) is greater than 0 is equivalent to the proposition that `r` itself is greater than 0. In other words, it asserts the consistency between the inequality comparisons in the context of nonnegative real numbers and their real parts.
More concisely: For any nonnegative real number `r`, the real part `↑r` is greater than 0 if and only if `r` itself is greater than 0.
|
ENNReal.coe_ne_top
theorem ENNReal.coe_ne_top : ∀ {r : NNReal}, ↑r ≠ ⊤
This theorem states that for every nonnegative real number `r` (represented as `NNReal`), the coextension of `r` is not equal to positive infinity (denoted by `⊤`). In other words, no nonnegative real number can be coextended to become positive infinity.
More concisely: For every non-negative real number `r`, `r` is not equal to positive infinity (⊤).
|
Mathlib.Data.ENNReal.Basic._auxLemma.10
theorem Mathlib.Data.ENNReal.Basic._auxLemma.10 : ∀ {r : ℝ}, (ENNReal.ofReal r < ⊤) = True
The theorem `Mathlib.Data.ENNReal.Basic._auxLemma.10` states that the function `ENNReal.ofReal`, when applied to any real number `r`, always yields a value that is less than positive infinity. This holds true for every real number `r`. Here, `ENNReal.ofReal` is a function that takes as input a real number and returns a nonnegative extended real number, or zero if the input is negative. The result less than positive infinity means the output of the function is always a finite number.
More concisely: For all real numbers `r`, the function `ENNReal.ofReal r` returns a finite extended real number.
|
ENNReal.coe_one
theorem ENNReal.coe_one : ↑1 = 1
This theorem states that the coercion of the integer 1 to the extended non-negative real number type (`ENNReal`) results in the same number, 1. In other words, when 1 is interpreted as an extended non-negative real number, it still remains 1.
More concisely: The theorem asserts that the coercion of the integer 1 to the type of extended non-negative real numbers is the identity function.
|
ENNReal.two_ne_top
theorem ENNReal.two_ne_top : 2 ≠ ⊤
This theorem states that the number 2 is not equal to infinity (denoted by ⊤) in the extended non-negative real numbers, abbreviated as ENNReal. In other words, in the context of the non-negative real numbers expanded to include infinity, 2 is finite and is distinct from the concept of infinity.
More concisely: The theorem asserts that 2 is distinct from infinity in the extended non-negative real numbers.
|
ENNReal.coe_le_coe_of_le
theorem ENNReal.coe_le_coe_of_le : ∀ {r q : NNReal}, r ≤ q → ↑r ≤ ↑q
This theorem states that for any two nonnegative real numbers `r` and `q`, if `r` is less than or equal to `q`, then the real number corresponding to `r` is also less than or equal to the real number corresponding to `q`. This is essentially the converse direction of the theorem `ENNReal.coe_le_coe`.
More concisely: If `r` is a nonnegative real number and `r <= q` for some nonnegative real number `q`, then the real number representation of `r` is less than or equal to the real number representation of `q`.
|
ENNReal.top_ne_coe
theorem ENNReal.top_ne_coe : ∀ {r : NNReal}, ⊤ ≠ ↑r
This theorem states that for any nonnegative real number `r`, the extended nonnegative real number representation of `r` (denoted by `↑r`) is never equal to infinity (denoted by `⊤`). In other words, no matter what nonnegative real number we choose, its corresponding extended nonnegative real number is always finite.
More concisely: For all non-negative real numbers r, ↑r ≠ ⊤.
|
ENNReal.ofReal_ne_top
theorem ENNReal.ofReal_ne_top : ∀ {r : ℝ}, ENNReal.ofReal r ≠ ⊤
The theorem `ENNReal.ofReal_ne_top` states that for every real number `r`, the function `ENNReal.ofReal` applied to `r` never equals `∞` (infinity). In other words, when any real number is passed into the `ENNReal.ofReal` function (which returns the number itself if it is nonnegative, or `0` if it's negative), the outcome will never be infinity.
More concisely: For all real numbers r, ENNReal.ofReal r is finite.
|
ENNReal.toReal_eq_zero_iff
theorem ENNReal.toReal_eq_zero_iff : ∀ (x : ENNReal), x.toReal = 0 ↔ x = 0 ∨ x = ⊤
This theorem states that for any extended nonnegative real number `x`, the real number equivalent of `x` is zero if and only if `x` itself is zero or `x` is infinity. In other words, it says that an extended nonnegative real number is mapped to zero in the real number system if and only if it is either zero or infinity in the extended nonnegative real number system.
More concisely: An extended nonnegative real number maps to zero in the real number system if and only if it is zero or infinity in the extended nonnegative real number system.
|
ENNReal.zero_toReal
theorem ENNReal.zero_toReal : 0.toReal = 0
This theorem asserts that the real number representation of the number zero in extended non-negative real numbers (ENNReal), denoted as `0.toReal`, is equal to zero. In other words, when the extended non-negative real number zero is converted to a real number, the result is also zero.
More concisely: The theorem asserts that `0.toReal` equals zero in the context of extended non-negative real numbers.
|
Mathlib.Data.ENNReal.Basic._auxLemma.37
theorem Mathlib.Data.ENNReal.Basic._auxLemma.37 : ∀ {p : NNReal}, (↑p < 1) = (p < 1)
This theorem states that for every nonnegative real number `p` (denoted as `NNReal`), the condition of `p` being less than 1 when promoted (`↑p`) to a nonnegative extended real number is equivalent to `p` being less than 1 as a nonnegative real number. Essentially, this shows that the inequality relationship `< 1` stays consistent when `NNReal` values are converted to extended nonnegative real numbers.
More concisely: For every nonnegative real number `p`, `p < 1` if and only if `↑p < 1` in the extended nonnegative real numbers.
|
ENNReal.lt_iff_exists_nnreal_btwn
theorem ENNReal.lt_iff_exists_nnreal_btwn : ∀ {a b : ENNReal}, a < b ↔ ∃ r, a < ↑r ∧ ↑r < b
This theorem states that for any two extended nonnegative real numbers `a` and `b`, `a` is less than `b` if and only if there exists a nonnegative real number `r` such that `a` is less than `r` and `r` is less than `b`. This means that between any two distinct extended nonnegative real numbers, we can always find a nonnegative real number. This is a formalization of the concept that the real numbers are densely ordered.
More concisely: For any extended nonnegative real numbers `a` and `b`, `a` < `b` if and only if there exists a nonnegative real number `r` such that `a` < `r` and `r` < `b`.
|
ENNReal.coe_toReal
theorem ENNReal.coe_toReal : ∀ (r : NNReal), (↑r).toReal = ↑r
This theorem, `ENNReal.coe_toReal`, states that for every nonnegative real number `r`, the real part obtained from the natural number (integer) coercion of `r` is equal to the integer coercion of `r` itself. In other words, applying the `toReal` function to the natural number created by coercing `r` will not affect the value, it will still remain as the original `r`. This ensures that we can safely convert a nonnegative real number to an integer and back without loss of information.
More concisely: For all non-negative real numbers r, the real part of the coercion of r to a natural number is equal to the coercion of r itself. In Lean, this is expressed as `ENNReal.coe_toReal r = r`.
|
ENNReal.coe_lt_top
theorem ENNReal.coe_lt_top : ∀ {r : NNReal}, ↑r < ⊤
This theorem states that for every nonnegative real number `r` (denoted as `NNReal`), the co-domain of `r` is less than infinity. In mathematical terms, this theorem asserts that the value of any nonnegative real number is always finite, i.e., it is always less than infinity (denoted by `⊤`).
More concisely: Every non-negative real number is finite.
Or equivalently:
The co-domain of every non-negative real number is bounded above.
|
ENNReal.toReal_ofReal
theorem ENNReal.toReal_ofReal : ∀ {r : ℝ}, 0 ≤ r → (ENNReal.ofReal r).toReal = r
This theorem states that for all real numbers `r`, if `r` is nonnegative (i.e., `r` is greater than or equal to 0), then the function `ENNReal.ofReal`, which maps `r` to the extended nonnegative real numbers, followed by the conversion back to the real numbers (`toReal`), is equal to the original real number `r`. In other words, the conversions from real numbers to extended nonnegative real numbers and then back to real numbers is an identity operation for nonnegative real numbers.
More concisely: For all real numbers `r` ≥ 0, `ENNReal.ofReal r = r` holds. (Or equivalently, `toReal (ENNReal.ofReal r) = r`.)
|
ENNReal.coe_lt_coe
theorem ENNReal.coe_lt_coe : ∀ {r q : NNReal}, ↑r < ↑q ↔ r < q
This theorem states that for any two non-negative real numbers `r` and `q`, the inequality `r < q` holds if and only if the same inequality holds after applying the coercion operation to `r` and `q` (denoted by `↑r < ↑q`). In other words, the ordering between `r` and `q` is preserved under the coercion from non-negative real numbers to extended non-negative real numbers.
More concisely: For any non-negative real numbers `r` and `q`, `r < q` if and only if `↑r < ↑q`.
|
Mathlib.Data.ENNReal.Basic._auxLemma.2
theorem Mathlib.Data.ENNReal.Basic._auxLemma.2 : ∀ {a : ENNReal}, (0 ≤ a.toReal) = True
This theorem states that for every extended nonnegative real number `a`, the property that `a` converted to a real number is greater than or equal to 0 is always true. In other words, the theorem asserts that any element of the extended nonnegative real numbers, when interpreted as a real number, is always nonnegative. The extended nonnegative real numbers are usually denoted as [0, ∞], and are relevant as the codomain of a measure.
More concisely: For all extended nonnegative real numbers `a`, `a` as a real number is non-negative.
|
Mathlib.Data.ENNReal.Basic._auxLemma.39
theorem Mathlib.Data.ENNReal.Basic._auxLemma.39 : ∀ (n : ℕ), (↑n = ⊤) = False
This theorem states that for any natural number `n`, it is not possible for the real number representation of `n` to be infinity (`⊤`). In other words, no natural number can be equivalent to infinity when converted into the set of extended non-negative real numbers.
More concisely: For any natural number `n`, `n` is not equal to infinity (`⊤`) in the set of extended non-negative real numbers.
|
Mathlib.Data.ENNReal.Basic._auxLemma.18
theorem Mathlib.Data.ENNReal.Basic._auxLemma.18 : (0 < ⊤) = True
This theorem, named `Mathlib.Data.ENNReal.Basic._auxLemma.18`, states that the positive infinity (`⊤`) is greater than zero. In mathematical terms, the inequality `0 < ⊤` is true. This theorem comes from the `Mathlib.Data.ENNReal.Basic` collection of lemmas and theorems in Lean 4.
More concisely: The theorem `Mathlib.Data.ENNReal.Basic._auxLemma.18` in Lean 4 asserts that 0 is less than positive infinity (0 < ⊤).
|
ENNReal.inv_smul_le_iff_of_pos
theorem ENNReal.inv_smul_le_iff_of_pos :
∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α]
[inst_2 : Preorder β] [inst_3 : MulAction α β] [inst_4 : PosSMulMono α β] [inst_5 : PosSMulReflectLE α β],
0 < a → (a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂)
This theorem, known as `ENNReal.inv_smul_le_iff_of_pos`, states that for any types `α` and `β`, variables `a` in `α` and `b₁`, `b₂` in `β`, given five instances involving `α` and `β` that include a group with zero, preorders, an action of `α` on `β`, positive scaling is monotone, and positive scaling reflects less than or equal to, if `a` is greater than zero, then `a` to the power of negative one (the multiplicative inverse of `a`) scaling `b₁` is less than or equal to `b₂` if and only if `b₁` is less than or equal to `a` scaling `b₂`. In mathematical notation, given 0 < a, then a⁻¹ * b₁ ≤ b₂ if and only if b₁ ≤ a * b₂.
More concisely: For any types `α` and `β` with a group `α` having zero, and an action of `α` on `β` such that positive scaling is monotone and reflects less than or equal to, if `a` is a positive element in `α`, then `a`'s multiplicative inverse scales `b₁` less than or equal to `b₂` if and only if `b₁` is less than or equal to `a` scaling `b₂`.
|
ENNReal.toReal_nat
theorem ENNReal.toReal_nat : ∀ (n : ℕ), (↑n).toReal = ↑n
This theorem states that for every natural number 'n', the real number equivalent of 'n' (obtained by typecasting 'n' to a real number), when converted back to a non-negative real number (ENNReal), remains equal to the original natural number 'n'. In other words, the processes of typecasting a natural number to a real number and then converting it to a non-negative real number do not change the value of the original natural number.
More concisely: For every natural number n, the conversion of n to an ENNReal and back to a real number equals the original natural number.
|
ENNReal.ofReal_zero
theorem ENNReal.ofReal_zero : ENNReal.ofReal 0 = 0
This theorem states that when the function `ENNReal.ofReal` is applied to the real number `0`, it returns `0`. This function is defined to return the input if it is nonnegative, and `0` otherwise, so in this case, because `0` is nonnegative, it should return `0`.
More concisely: The theorem asserts that `ENNReal.ofReal 0 = 0`.
|
ENNReal.le_of_forall_pos_le_add
theorem ENNReal.le_of_forall_pos_le_add : ∀ {a b : ENNReal}, (∀ (ε : NNReal), 0 < ε → b < ⊤ → a ≤ b + ↑ε) → a ≤ b := by
sorry
This theorem states that for all extended nonnegative real numbers 'a' and 'b', if for every positive nonnegative real number 'ε', 'b' is less than infinity and 'a' is less than or equal to 'b' plus 'ε', then 'a' is less than or equal to 'b'. In other words, if 'a' is less than 'b' plus any small positive number and 'b' is finite, then 'a' is less than or equal to 'b'. This is a common type of limit argument in mathematical analysis.
More concisely: If for all positive ε, a ≤ b + ε implies a ≤ b for extended nonnegative real numbers a and b with b finite, then a ≤ b.
|
ENNReal.ofReal_coe_nnreal
theorem ENNReal.ofReal_coe_nnreal : ∀ {p : NNReal}, ENNReal.ofReal ↑p = ↑p
This theorem states that for any nonnegative real number `p` (denoted as `NNReal`), the function `ENNReal.ofReal` applied to the coercion of `p` to a real number will yield the same result as simply coercing `p` to an extended nonnegative real number (denoted as `ENNReal`). In other words, the `ENNReal.ofReal` function behaves as expected on nonnegative real numbers when they are interpreted as extended nonnegative real numbers.
More concisely: For any non-negative real number `p`, `ENNReal.ofReal (realCoerce p) = ENNReal p`.
|
ENNReal.coe_nnreal_eq
theorem ENNReal.coe_nnreal_eq : ∀ (r : NNReal), ↑r = ENNReal.ofReal ↑r
This theorem states that for every nonnegative real number `r` (denoted as `NNReal`), the coercion of `r` to extended nonnegative real numbers (`ENNReal`) is equal to the result of applying the `ENNReal.ofReal` function to the coercion of `r` to real numbers. In mathematical terms, for all `r` in nonnegative real numbers, we have that the image of `r` under the inclusion map into the extended nonnegative real numbers is the same as the image of `r` under the map `ENNReal.ofReal`, after `r` has been identified with its corresponding real number.
More concisely: For every non-negative real number `r`, `ENNReal.ofReal (coercion r to Real) = coercion r to ENNReal`.
|
Mathlib.Data.ENNReal.Basic._auxLemma.16
theorem Mathlib.Data.ENNReal.Basic._auxLemma.16 : (1 = ⊤) = False
This theorem states that the number 1 is not equal to infinity (∞), when working in the context of extended non-negative real numbers (ENNReal). In other words, it asserts the falsehood of the claim "1 equals ∞".
More concisely: The theorem asserts that 1 ≠ ∞ in the context of extended non-negative real numbers.
|
Mathlib.Data.ENNReal.Basic._auxLemma.14
theorem Mathlib.Data.ENNReal.Basic._auxLemma.14 : (0 = ⊤) = False
This theorem, `Mathlib.Data.ENNReal.Basic._auxLemma.14`, states that zero is not equal to infinity. In other words, it denies the equality between zero and infinity in the context of extended non-negative real numbers.
More concisely: Zero is not equal to infinity in the context of extended non-negative real numbers.
|
ENNReal.exists_nat_gt
theorem ENNReal.exists_nat_gt : ∀ {r : ENNReal}, r ≠ ⊤ → ∃ n, r < ↑n
This theorem states that for every extended nonnegative real number `r` that is not equal to infinity, there exists a natural number `n` such that `r` is less than `n`. In other words, any finite extended nonnegative real number is strictly less than some natural number.
More concisely: For every finite extended non-negative real number `r`, there exists a natural number `n` such that `r` < `n`.
|
ENNReal.toNNReal_eq_zero_iff
theorem ENNReal.toNNReal_eq_zero_iff : ∀ (x : ENNReal), x.toNNReal = 0 ↔ x = 0 ∨ x = ⊤
This theorem states that for any extended nonnegative real number `x`, the function `toNNReal` applied to `x` equals zero if and only if `x` itself equals zero or `x` equals infinity. Informally, it asserts that in the set of extended nonnegative real numbers (which includes 0, positive reals, and infinity), the only elements that map to zero in the nonnegative real numbers are 0 and infinity.
More concisely: For any extended nonnegative real number `x`, `toNNReal x = 0` if and only if `x = 0` or `x = ∞`.
|
ENNReal.toNNReal_eq_toNNReal_iff'
theorem ENNReal.toNNReal_eq_toNNReal_iff' : ∀ {x y : ENNReal}, x ≠ ⊤ → y ≠ ⊤ → (x.toNNReal = y.toNNReal ↔ x = y) := by
sorry
This theorem states that for any two extended nonnegative real numbers `x` and `y`, as long as neither `x` nor `y` are equal to positive infinity, `x.toNNReal` being equal to `y.toNNReal` is equivalent to `x` being equal to `y`. In other words, if two extended nonnegative real numbers are not infinity, then their conversion to nonnegative real numbers will maintain their equality.
More concisely: For extended nonnegative real numbers `x` and `y`, if `x` and `y` are finite, then `x = y` if and only if `x.toNNReal = y.toNNReal`.
|
Mathlib.Data.ENNReal.Basic._auxLemma.32
theorem Mathlib.Data.ENNReal.Basic._auxLemma.32 : (2 = ⊤) = False
This theorem states that the number 2 is not equal to infinity. In Lean, "⊤" is used to represent infinity, usually in the context of extended non-negative real numbers (where real numbers are extended by adding infinity as a value). The proof, which is not shown here, establishes that 2 cannot be the same as infinity, which is intuitively obvious in the realm of real numbers.
More concisely: The theorem asserts that 2 is not equal to infinity (2 ≠ ⊤) in the context of extended non-negative real numbers.
|
Mathlib.Data.ENNReal.Basic._auxLemma.6
theorem Mathlib.Data.ENNReal.Basic._auxLemma.6 : ∀ {r : NNReal}, (↑r = ⊤) = False
This theorem states that for all nonnegative real numbers (`NNReal`), it is false that they are equal to positive infinity (`⊤`). In other words, no nonnegative real number can be equal to positive infinity.
More concisely: For all nonnegative real numbers `x`, `x` is not equal to positive infinity (`⊤`).
|
Mathlib.Data.ENNReal.Basic._auxLemma.9
theorem Mathlib.Data.ENNReal.Basic._auxLemma.9 : ∀ {r : ℝ}, (ENNReal.ofReal r = ⊤) = False
The theorem `Mathlib.Data.ENNReal.Basic._auxLemma.9` states that for any real number `r`, the result of the function `ENNReal.ofReal r` can never be infinity (or `⊤` in Lean 4 notation). In other words, when a real number is converted to an extended nonnegative real number using the `ofReal` function, the result is never infinity.
More concisely: For any real number r, the result of the function `ENNReal.ofReal r` is finite.
|
ENNReal.coe_toNNReal
theorem ENNReal.coe_toNNReal : ∀ {a : ENNReal}, a ≠ ⊤ → ↑a.toNNReal = a
This theorem states that for all elements `a` of the extended nonnegative real numbers (`ENNReal`), as long as `a` is not infinite (`∞`), then the nonnegative real number corresponding to `a` (obtained using `toNNReal`) when converted back to `ENNReal` (`↑a.toNNReal`) is still equal to `a`. In other words, for any non-infinite extended nonnegative real number, we can convert it into a nonnegative real number and back without changing its value.
More concisely: For all `a` in `ENNReal` that are finite, `↑(toNNReal a) = a`.
|
ENNReal.coe_pos
theorem ENNReal.coe_pos : ∀ {r : NNReal}, 0 < ↑r ↔ 0 < r
The theorem `ENNReal.coe_pos` states that for any nonnegative real number `r` (denoted as `NNReal`), the positivity of the embedding (or "coercion") of `r` into the extended nonnegative real numbers (that is, `0 < ↑r`) is equivalent to the positivity of `r` itself (that is, `0 < r`). In other words, a nonnegative real number `r` is positive if and only if its corresponding extended nonnegative real number is also positive.
More concisely: The embedding of a non-negative real number into the extended non-negative reals is positive if and only if the original number is positive.
|
Mathlib.Data.ENNReal.Basic._auxLemma.45
theorem Mathlib.Data.ENNReal.Basic._auxLemma.45 :
∀ {β : Type u_2} {ι : Sort u_4} (s : Set β) (t : ι → Set β), ⋃ i, s ∩ t i = s ∩ ⋃ i, t i
This theorem states that for any type `β`, and for any type `ι`, if `s` is a set of `β` and `t` is a function from `ι` to a set of `β`, then the union over all `i` of the intersection of `s` and `t i` is equal to the intersection of `s` and the union over all `i` of `t i`. In mathematical terms, this theorem asserts that $\bigcup_{i} (s \cap t_i) = s \cap \bigcup_{i} t_i$. This is a property of the interactions between union and intersection operations in set theory.
More concisely: For any types `β` and `ι`, and sets `s` of `β` and function `t` from `ι` to sets of `β`, the union of intersections of `s` with each `t(i)` equals the intersection of `s` with the union of all `t(i)`. Mathematically: $\bigcup\_{i} (s \cap t\_i) = s \cap \bigcup\_{i} t\_i$.
|
ENNReal.coe_zero
theorem ENNReal.coe_zero : ↑0 = 0
This theorem is stating that the coercion of zero from the extended non-negative reals (denoted by `ENNReal` in Lean) to some other type is equal to zero. In other words, when zero is considered as an element of the extended non-negative reals, and then translated ("coerced") into another type, it remains zero.
More concisely: The theorem asserts that the coercion of the real number zero from the extended non-negative reals to any other type equals zero.
|
Mathlib.Data.ENNReal.Basic._auxLemma.15
theorem Mathlib.Data.ENNReal.Basic._auxLemma.15 : (⊤ = 0) = False
This theorem states that infinity, designated as "⊤" in the Lean 4 language, is not equal to zero. In other words, the proposition that infinity is equal to zero is false. This is aligned with established mathematical principles, where infinity represents an unbounded quantity that is greater than any finite number, and hence cannot be equal to zero.
More concisely: In Lean 4, the proposition that infinity (⊤) equals zero is false.
|
ENNReal.coe_eq_zero
theorem ENNReal.coe_eq_zero : ∀ {r : NNReal}, ↑r = 0 ↔ r = 0
This theorem states that for any nonnegative real number `r` (of type `NNReal`), the coercion of `r` to an extended nonnegative real number (`ENNReal`) equals zero if and only if `r` itself equals zero. In mathematical terms, let `r` be a nonnegative real number. This result tells us that `r` maps to zero in the extended nonnegative real numbers exactly when `r` is zero.
More concisely: For any nonnegative real number `r`, `r` maps to zero in the extended nonnegative real numbers if and only if `r` equals zero.
|
ENNReal.zero_lt_top
theorem ENNReal.zero_lt_top : 0 < ⊤
This theorem states that zero is less than infinity in the set of extended non-negative real numbers. In mathematical terms, it confirms that 0 is strictly less than infinity (0 < ∞) when considering the spectrum that includes all non-negative real values as well as the concept of infinity.
More concisely: In the extended non-negative real numbers, 0 is strictly less than infinity (0 < ∞).
|
Mathlib.Data.ENNReal.Basic._auxLemma.21
theorem Mathlib.Data.ENNReal.Basic._auxLemma.21 : ∀ {r : NNReal}, (↑r = 0) = (r = 0)
This theorem states that for all non-negative real numbers `r` (denoted as `NNReal`), the condition of `r` being equal to zero in its natural number embedding (notated as `↑r`) is equivalent to `r` being equal to zero. In other words, a non-negative real number `r` is zero if and only if its corresponding natural number is zero.
More concisely: For every non-negative real number `r`, `↑r = 0` if and only if `r = 0`.
|
Mathlib.Data.ENNReal.Basic._auxLemma.19
theorem Mathlib.Data.ENNReal.Basic._auxLemma.19 : ∀ {r q : NNReal}, (↑r ≤ ↑q) = (r ≤ q)
This theorem, which belongs to the basic functions of the extended nonnegative real numbers module in Mathlib, states that for any two nonnegative real numbers `r` and `q`, the statement "the real number component of `r` is less than or equal to the real number component of `q`" is equivalent to "r is less than or equal to q". In other words, the ordering of their real components is the same as the ordering of the nonnegative real numbers themselves.
More concisely: For all non-negative real numbers r and q, r ≤ q if and only if reals.r <= reals.q.
|
ENNReal.some_eq_coe
theorem ENNReal.some_eq_coe : ∀ (a : NNReal), some a = ↑a
This theorem states that for every nonnegative real number `a` (designated by `NNReal`), applying the `some` function to `a` gives the same result as applying the type coercion function (denoted by the up-arrow operator `↑`) to `a`. In other words, the `some` function and the type coercion function act equivalently on the set of nonnegative real numbers.
More concisely: For every non-negative real number `a`, `some a` is equal to the real number `↑a`.
|