EReal.le_neg_of_le_neg
theorem EReal.le_neg_of_le_neg : ∀ {a b : EReal}, a ≤ -b → b ≤ -a
This theorem states that for every two elements `a` and `b` from the EReal set, which represents all real numbers including negative infinity and positive infinity, if `a` is less than or equal to the negation of `b`, then `b` is less than or equal to the negation of `a`. This property is reflective of the order relationship in the extended real number system.
More concisely: For all `a, b` in EReal, `a <= -b <-> b <= -a` (if and only if).
|
EReal.preimage_coe_Iio
theorem EReal.preimage_coe_Iio : ∀ (y : ℝ), Real.toEReal ⁻¹' Set.Iio ↑y = Set.Iio y
The theorem `EReal.preimage_coe_Iio` states that for every real number `y`, the preimage of the set of values less than `y` under the mapping from reals to extended reals is equal to the set of real numbers less than `y`. In other words, if you take all the elements less than `y` in the space of extended real numbers, and map them back to the real numbers, you get exactly the set of real numbers less than `y`. This result is crucial in ensuring that our extension from real numbers to extended real numbers behaves as expected when dealing with sets and intervals.
More concisely: The preimage of the set of real numbers less than a real number `y` under the coercion from extended real numbers to real numbers is equal to the set of real numbers less than `y`.
|
EReal.coe_mul
theorem EReal.coe_mul : ∀ (x y : ℝ), ↑(x * y) = ↑x * ↑y
This theorem states that for any two real numbers `x` and `y`, the operation of multiplying them and then applying the coe (coercion) function is equivalent to first applying the coe function to each of them and then multiplying the results. In other words, the coe function distributes over multiplication in the set of real numbers. This can be expressed mathematically as: ∀(x, y ∈ ℝ), coe(x*y) = coe(x) * coe(y).
More concisely: The coercion function distributes over multiplication in the set of real numbers, i.e., for all `x, y ∈ ℝ`, `coe(x * y) = coe(x) * coe(y)`.
|
EReal.induction₂
theorem EReal.induction₂ :
∀ {P : EReal → EReal → Prop},
P ⊤ ⊤ →
(∀ (x : ℝ), 0 < x → P ⊤ ↑x) →
P ⊤ 0 →
(∀ x < 0, P ⊤ ↑x) →
P ⊤ ⊥ →
(∀ (x : ℝ), 0 < x → P ↑x ⊤) →
(∀ (x : ℝ), 0 < x → P ↑x ⊥) →
P 0 ⊤ →
(∀ (x y : ℝ), P ↑x ↑y) →
P 0 ⊥ →
(∀ x < 0, P ↑x ⊤) →
(∀ x < 0, P ↑x ⊥) →
P ⊥ ⊤ →
(∀ (x : ℝ), 0 < x → P ⊥ ↑x) →
P ⊥ 0 → (∀ x < 0, P ⊥ ↑x) → P ⊥ ⊥ → ∀ (x y : EReal), P x y
The theorem `EReal.induction₂` provides a principle of induction for pairs of values of type `EReal`, which extends the real numbers to include negative and positive infinity. The principle allows us to prove a property `P` for all pairs of `EReal` values, given that we know `P` holds for various specific cases. These cases include when both values are positive infinity, when one is positive infinity and the other is a positive real, when one is positive infinity and the other is zero, when one is positive infinity and the other is a negative real, and when one is positive infinity and the other is negative infinity, with similar cases for when one value is a positive real, zero, a negative real, or negative infinity. The principle also requires that `P` holds for all pairs of real numbers.
More concisely: The theorem `EReal.induction₂` asserts the preservation of a property `P` for all pairs of extended real numbers, where `P` holds for all real numbers and for specific cases of positive and negative infinities.
|
EReal.coe_mul_bot_of_pos
theorem EReal.coe_mul_bot_of_pos : ∀ {x : ℝ}, 0 < x → ↑x * ⊥ = ⊥
The theorem `EReal.coe_mul_bot_of_pos` states that for all real numbers `x`, if `x` is greater than 0, then the product of the extended real number representation of `x` and negative infinity (`⊥`) is negative infinity (`⊥`).
More concisely: For all real numbers `x` with `x > 0`, the product of `x` and negative infinity is negative infinity. (In mathematical notation: `(x : ℝ). 0 < x → x * ⊥ = ⊥`)
|
EReal.sign_mul_abs
theorem EReal.sign_mul_abs : ∀ (x : EReal), ↑(SignType.sign x) * ↑x.abs = x
This theorem states that for any extended real number `x` (which can range from negative infinity to positive infinity), the product of the sign of `x` and the absolute value of `x` is equal to `x` itself. Here, the sign of a number is defined as `1` if it's positive, `-1` if it's negative, and `0` if it's exactly `0`. The absolute value function maps `-∞` and `+∞` to `+∞`, and any real number to its absolute value. This theorem is analogous to the property of regular real numbers where a number is equal to the product of its sign and its absolute value.
More concisely: For any extended real number x, x = abs x * sign x.
|
EReal.neg_le_neg_iff
theorem EReal.neg_le_neg_iff : ∀ {a b : EReal}, -a ≤ -b ↔ b ≤ a
This theorem, `EReal.neg_le_neg_iff`, states that for every pair of elements `a` and `b` of the type `EReal` (which represents the extended real numbers, including positive and negative infinity), the negation of `a` is less than or equal to the negation of `b` if and only if `b` is less than or equal to `a`. This is a statement of the property of order reversal under negation for extended real numbers.
More concisely: For all `a` and `b` in `EReal`, `-a <= -b` if and only if `b <= a`.
|
EReal.induction₂_neg_left
theorem EReal.induction₂_neg_left :
∀ {P : EReal → EReal → Prop},
(∀ {x y : EReal}, P x y → P (-x) y) →
P ⊤ ⊤ →
(∀ (x : ℝ), 0 < x → P ⊤ ↑x) →
P ⊤ 0 →
(∀ x < 0, P ⊤ ↑x) →
P ⊤ ⊥ →
P 0 ⊤ →
P 0 ⊥ →
(∀ (x : ℝ), 0 < x → P ↑x ⊤) →
(∀ (x : ℝ), 0 < x → P ↑x ⊥) → (∀ (x y : ℝ), P ↑x ↑y) → ∀ (x y : EReal), P x y
This theorem is a form of induction on two extended real numbers (`EReal`), which can range from negative infinity to positive infinity. The theorem is called `EReal.induction₂_neg_left` and assumes that for any property `P`, if `P x y` is true then `P (-x) y` is also true for all `x` and `y`. The theorem then states that if `P` holds for several specific cases, namely positive infinity with positive infinity, positive infinity with positive real numbers, positive infinity with zero, etc., then `P` holds for all `x` and `y` in `EReal`. The specific cases also include zero with positive and negative infinity, and positive real numbers with positive infinity and negative infinity, as well as all pairs of real numbers.
More concisely: If `P(x, y)` holds for all `x, y` in `EReal` when `x = +\infty, y = +\infty`, `x = +\infty, y in \R`, `x = 0, y = +\infty`, `x in \R, y = +\infty`, and `x, y in \R` with `x <= y`, then `P` holds for all `x, y` in `EReal`.
|
EReal.add_lt_add
theorem EReal.add_lt_add : ∀ {x y z t : EReal}, x < y → z < t → x + z < y + t
This theorem states that for all extended real numbers `x`, `y`, `z`, and `t`, if `x` is less than `y` and `z` is less than `t`, then the sum of `x` and `z` is less than the sum of `y` and `t`. This theorem is a property of order in the set of extended real numbers, which contains all real numbers plus negative and positive infinity. This is similar to the property in real numbers where the sum of two smaller numbers is smaller than the sum of two larger numbers.
More concisely: For all extended real numbers x, y, z, and t, if x < y and z < t then x + z < y + t.
|
EReal.coe_strictMono
theorem EReal.coe_strictMono : StrictMono Real.toEReal
The theorem `EReal.coe_strictMono` asserts that the function `Real.toEReal`, which is the canonical inclusion from the real numbers to the extended real numbers, is strictly monotone. In other words, if `a` and `b` are real numbers with `a < b`, then `Real.toEReal a < Real.toEReal b`.
More concisely: The canonical inclusion `Real.toEReal` from the real numbers to the extended real numbers is a strictly increasing function.
|
EReal.preimage_coe_Ici
theorem EReal.preimage_coe_Ici : ∀ (x : ℝ), Real.toEReal ⁻¹' Set.Ici ↑x = Set.Ici x
This theorem is stating that for any real number 'x', the preimage of the interval [x, +∞) under the function that coverts real numbers to extended real numbers is equal to the interval [x, +∞) in the real numbers. In other words, when we convert each number in the real interval [x, +∞) to an extended real number, we get the same set as the original interval [x, +∞).
More concisely: For any real number x, the preimage of the interval [x, +∞) under the extension of the real numbers to the extended real numbers is equal to the interval [x, +∞) in the real numbers.
|
EReal.coe_pos
theorem EReal.coe_pos : ∀ {x : ℝ}, 0 < ↑x ↔ 0 < x
This theorem states that for any real number `x`, the property of the coersion of `x` being greater than 0 is equivalent to `x` itself being greater than 0. In mathematical terms, if `x` is a real number, then 0 being less than the coersion of `x` (notated as `↑x`) is equivalent to 0 being less than `x`.
More concisely: The theorem asserts that for any real number `x`, `0 < x` is equivalent to `0 < ↑x`.
|
EReal.sign_coe
theorem EReal.sign_coe : ∀ (x : ℝ), SignType.sign ↑x = SignType.sign x
This theorem states that for any real number `x`, the sign of the coerced value of `x` (interpreted as an element of an extended real number type, via `↑x`) is the same as the sign of `x` itself. Here, the sign of a number is defined as 1 if the number is positive, -1 if the number is negative, and 0 if the number is neither positive nor negative (i.e., it is zero). In other words, the process of coercing a real number to an extended real number does not change its sign.
More concisely: For any real number x, the sign of x and the sign of its coerced value ↑x as extended real numbers are equal.
|
EReal.coe_ne_top
theorem EReal.coe_ne_top : ∀ (x : ℝ), ↑x ≠ ⊤
This theorem states that for any real number `x`, the extended real number equivalent of `x` is not equal to positive infinity. Explicitly, this means that no matter what real number we choose, when we convert this real number into its extended real number form, it will never be equal to positive infinity.
More concisely: For every real number x, its extended real number equivalent is not equal to positive infinity.
|
EReal.coe_ennreal_injective
theorem EReal.coe_ennreal_injective : Function.Injective ENNReal.toEReal
The theorem `EReal.coe_ennreal_injective` states that the function `ENNReal.toEReal`, which is the canonical map converting nonnegative extended reals to extended reals, is injective. In other words, if `ENNReal.toEReal x = ENNReal.toEReal y`, then `x = y`. This means that no two different nonnegative extended reals map to the same extended real under this function.
More concisely: The theorem `EReal.coe_ennreal_injective` asserts that the function `ENNReal.toEReal` mapping non-negative extended reals to extended reals is an injection.
|
EReal.preimage_coe_Iic
theorem EReal.preimage_coe_Iic : ∀ (y : ℝ), Real.toEReal ⁻¹' Set.Iic ↑y = Set.Iic y
The theorem `EReal.preimage_coe_Iic` states that for any real number `y`, the preimage of the set of all extended real numbers less than or equal to `y` under the function mapping real numbers to extended real numbers, is equal to the set of all real numbers less than or equal to `y`. In other words, if we take a set of all extended real numbers less than or equal to a given real number `y`, convert each of those extended real numbers back to a real number (if possible), we would end up with the set of all real numbers less than or equal to `y`.
More concisely: The preimage of the set of real numbers less than or equal to a real number `y` under the extension of the real numbers to the extended real numbers is equal to the set of real numbers less than or equal to `y`.
|
EReal.induction₂_symm
theorem EReal.induction₂_symm :
∀ {P : EReal → EReal → Prop},
(∀ {x y : EReal}, P x y → P y x) →
P ⊤ ⊤ →
(∀ (x : ℝ), 0 < x → P ⊤ ↑x) →
P ⊤ 0 →
(∀ x < 0, P ⊤ ↑x) →
P ⊤ ⊥ →
(∀ (x : ℝ), 0 < x → P ↑x ⊥) →
(∀ (x y : ℝ), P ↑x ↑y) → P 0 ⊥ → (∀ x < 0, P ↑x ⊥) → P ⊥ ⊥ → ∀ (x y : EReal), P x y
This theorem is essentially a method of induction on two extended real numbers (`EReal`s), given some symmetric property `P`. In this context, an `EReal` is an extension of the real numbers that also includes positive and negative infinity (`⊤` and `⊥` respectively).
The theorem says that if a property `P` holds for all pairs of `EReal`s `(x, y)` whenever it holds for `(y, x)`, and if `P` holds for the pairs `(⊤, ⊤)`, `(⊤, x)` for all positive real `x`, `(⊤, 0)`, `(⊤, x)` for all negative real `x`, `(⊤, ⊥)`, `(x, ⊥)` for all positive real `x`, `(x, y)` for all real `x` and `y`, `(0, ⊥)`, `(x, ⊥)` for all negative real `x`, and `(⊥, ⊥)`, then `P` must hold for all pairs of `EReal`s `(x, y)`.
It's a way of breaking down a property over the extended real numbers into several cases, involving both finite and infinite values, and using the symmetry of the property to reduce the number of cases that have to be checked directly.
More concisely: If a symmetric property holds for all finite and infinite real numbers `(x, y)` and their corresponding reflections `(y, x)`, including the cases `(⊤, ⊤)`, `(⊤, x)` for all `x ∈ ℝ`, `(⊤, ⊥)`, `(x, ⊥)` for all `x ∈ ℝ`, and `(⊥, ⊥)`, then it holds for all pairs `(x, y)` of extended real numbers.
|
EReal.add_lt_add_of_lt_of_le
theorem EReal.add_lt_add_of_lt_of_le : ∀ {x y z t : EReal}, x < y → z ≤ t → z ≠ ⊥ → t ≠ ⊤ → x + z < y + t
This theorem states that for all extended real numbers `x`, `y`, `z`, and `t`, if `x` is less than `y` and `z` is less than or equal to `t`, and provided that `z` is not negative infinity and `t` is not positive infinity, then the sum of `x` and `z` is less than the sum of `y` and `t`. This can be understood as a version of the property that adding a smaller number to both sides of an inequality preserves the inequality, extended to the context of extended real numbers, with specific constraints on dealing with infinities.
More concisely: For all extended real numbers x, y, z, and t, if x < y and z <= t with z not being negative infinity and t not being positive infinity, then x + z < y + t.
|
EReal.coe_lt_coe_iff
theorem EReal.coe_lt_coe_iff : ∀ {x y : ℝ}, ↑x < ↑y ↔ x < y
This theorem states that for any two real numbers `x` and `y`, the statement that the embedding of `x` is less than the embedding of `y` is equivalent to the statement that `x` is less than `y`. In other words, it describes the relationship between the order of real numbers and their corresponding elements in the extended real number system. The embeddings referred to here are the natural mappings from the set of real numbers to the set of extended real numbers.
More concisely: The theorem asserts that for real numbers x and y, x < y if and only if x.__le__(y) holds in the extended real numbers.
|
EReal.coe_ennreal_zero
theorem EReal.coe_ennreal_zero : ↑0 = 0
This theorem states that the embedding of zero from the extended non-negative real numbers (`ennreal`) into the extended real numbers (`EReal`) is zero. In other words, if we cast zero as an extended non-negative real number into the extended real numbers, we still get zero.
More concisely: The theorem asserts that the conversion of the natural number zero to an extended non-negative real number, and then to an extended real number, equals zero.
|
EReal.bot_lt_coe
theorem EReal.bot_lt_coe : ∀ (x : ℝ), ⊥ < ↑x
This theorem states that for any real number `x`, the extended real number corresponding to negative infinity (represented here as ⊥) is less than the extended real number representation of `x`. In mathematical terms, it's stating that -∞ < `x` for any real number `x`.
More concisely: For any real number `x`, negative infinity (⊥) is strictly smaller than `x`.
|
Mathlib.Data.Real.EReal._auxLemma.2
theorem Mathlib.Data.Real.EReal._auxLemma.2 : ∀ {x y : ℝ}, (↑x < ↑y) = (x < y)
This theorem, `Mathlib.Data.Real.EReal._auxLemma.2`, states that for any two real numbers `x` and `y`, the inequality between their eReal (extended real number) representations, `↑x < ↑y`, is equivalent to the inequality between the numbers themselves, `x < y`. Essentially, this theorem asserts the preservation of inequality when converting from real numbers to extended real numbers.
More concisely: For any real numbers x and y, the extended real number inequalities ↑x < ↑y are equivalent to the real number inequalities x < y.
|
EReal.mul_comm
theorem EReal.mul_comm : ∀ (x y : EReal), x * y = y * x
This theorem states that multiplication of extended real numbers, i.e., numbers that can range from negative infinity to positive infinity, is commutative. In other words, for any two extended real numbers `x` and `y`, the result of multiplying `x` by `y` is the same as the result of multiplying `y` by `x`.
More concisely: For all extended real numbers x and y, x * y = y * x.
|
EReal.neg_le
theorem EReal.neg_le : ∀ {a b : EReal}, -a ≤ b ↔ -b ≤ a
This theorem states that for any two extended real numbers `a` and `b`, the negation of `a` is less than or equal to `b` if and only if the negation of `b` is less than or equal to `a`. In other words, it establishes a property of order reversal under negation in the extended real number system.
More concisely: For any extended real numbers `a` and `b`, the negation of `a` is less than or equal to `b` if and only if the negation of `b` is less than or equal to `a`. Equivalently, `-a <= b <-> -b <= a`.
|
EReal.exists_between_coe_real
theorem EReal.exists_between_coe_real : ∀ {x z : EReal}, x < z → ∃ y, x < ↑y ∧ ↑y < z
The theorem `EReal.exists_between_coe_real` states that for any two extended real numbers `x` and `z` (represented as `EReal`), if `x` is less than `z`, then there exists a regular real number `y` (represented as `↑y` after being coerced from real numbers to `EReal`), such that `x` is less than `y` and `y` is less than `z`. This means that between any two distinct extended real numbers, we can always find a regular real number.
More concisely: For any two extended real numbers `x` and `z` with `x < z`, there exists a regular real number `y` such that `x < y < z`.
|
EReal.coe_lt_top
theorem EReal.coe_lt_top : ∀ (x : ℝ), ↑x < ⊤
This theorem states that for any real number `x`, the extended real number representation of `x` is always less than positive infinity. In mathematical terms, for every real number `x`, it holds that `x` is strictly less than positive infinity when `x` is interpreted in the extended real number system.
More concisely: For every real number `x`, `x` is strictly less than positive infinity in the extended real number system.
|
EReal.preimage_coe_Iio_top
theorem EReal.preimage_coe_Iio_top : Real.toEReal ⁻¹' Set.Iio ⊤ = Set.univ
This theorem states that the preimage of the left-infinite right-open interval (`Set.Iio`) that ends at positive infinity (`⊤`), under the function that maps real numbers (`ℝ`) to extended real numbers (`EReal`), is the universal set (`Set.univ`). In other words, if we map all real numbers to extended real numbers and consider those which are less than positive infinity, we end up with all real numbers. This highlights that all real numbers are also a part of the extended real number system which includes positive and negative infinity.
More concisely: The preimage of `Set.Iio ⊤` under the function from `ℝ` to `EReal` equals `Set.univ`.
|
EReal.induction₂_symm_neg
theorem EReal.induction₂_symm_neg :
∀ {P : EReal → EReal → Prop},
(∀ {x y : EReal}, P x y → P y x) →
(∀ {x y : EReal}, P x y → P (-x) y) →
P ⊤ ⊤ → (∀ (x : ℝ), 0 < x → P ⊤ ↑x) → P ⊤ 0 → (∀ (x y : ℝ), P ↑x ↑y) → ∀ (x y : EReal), P x y
This theorem is a method for inductive reasoning over two extended real numbers (Ereal), considering their possible minus infinity, zero, positive real, and positive infinity values. The property `P` under consideration should satisfy three conditions: it is symmetric (if `P x y` then `P y x`), it is negation-invariant (if `P x y` then `P -x y`), and it holds for different combination of values of extended real numbers such as both being infinity, one being infinity and the other being a positive real number or zero, and both being real numbers. If these conditions are met, then the property `P` holds for any two extended real numbers `x` and `y`.
More concisely: If `P` is a symmetric and negation-invariant relation on extended real numbers satisfying `P x y => P y x` for all `x, y ∈ Ereal` with `P` holding for all combinations of infinity, positive real numbers, and zero, then `P` holds for all `x, y ∈ Ereal`.
|
EReal.coe_ennreal_strictMono
theorem EReal.coe_ennreal_strictMono : StrictMono ENNReal.toEReal
The theorem `EReal.coe_ennreal_strictMono` states that the function `ENNReal.toEReal`, which is the canonical map from nonnegative extended real numbers (`ENNReal`) to extended real numbers (`EReal`), is strictly monotone. In other words, for any two nonnegative extended real numbers `a` and `b`, if `a` is less than `b`, then the image of `a` under the function `ENNReal.toEReal` is less than the image of `b` under the same function.
More concisely: The function `ENNReal.toEReal` maps nonnegative extended real numbers to extended real numbers strictly increasing their values.
|
EReal.exists_rat_btwn_of_lt
theorem EReal.exists_rat_btwn_of_lt : ∀ {a b : EReal}, a < b → ∃ x, a < ↑↑x ∧ ↑↑x < b
This theorem states that for any two extended real numbers `a` and `b` such that `a` is less than `b`, there exists a rational number `x` such that `a` is less than `x` and `x` is less than `b`. In other words, between any two distinct extended real numbers, one can always find a rational number. This is a formal version of the mathematical property that the rational numbers are dense in the extended real numbers.
More concisely: For any extended real numbers `a` and `b` with `a < b`, there exists a rational number `x` such that `a < x < b`.
|
Mathlib.Data.Real.EReal._auxLemma.6
theorem Mathlib.Data.Real.EReal._auxLemma.6 : ∀ (x : ℝ), (↑x = ⊥) = False
This theorem, from the Mathlib library for the Lean theorem prover, states that the real number 'x' when lifted to the extended real number line, cannot be equal to negative infinity. In other words, any real number 'x', when considered as an extended real number, is always finite and it's impossible for it to be negative infinity. This holds true for all real numbers 'x'.
More concisely: The real number 'x' is never equal to negative infinity when considered as an extended real number.
|
EReal.top_mul_coe_of_pos
theorem EReal.top_mul_coe_of_pos : ∀ {x : ℝ}, 0 < x → ⊤ * ↑x = ⊤
This theorem states that for every real number `x`, if `x` is greater than zero, then the product of the extended real number positive infinity (`⊤`) and the coercion of `x` to an extended real number equals positive infinity (`⊤`). In other words, any positive real number, when multiplied with positive infinity, results in positive infinity in the context of extended real numbers.
More concisely: For every real number `x > 0`, `x * ⊤ = ⊤` in the context of extended real numbers.
|
EReal.preimage_coe_Ioi
theorem EReal.preimage_coe_Ioi : ∀ (x : ℝ), Real.toEReal ⁻¹' Set.Ioi ↑x = Set.Ioi x
This theorem states that for every real number `x`, the preimage of the interval `(x, +∞)` under the canonical inclusion from real numbers to extended real numbers is exactly the interval `(x, +∞)`. In other words, the canonical inclusion maps the interval `(x, +∞)` of real numbers onto the interval `(x, +∞)` of extended real numbers.
More concisely: The canonical inclusion map from real numbers to extended real numbers maps the open interval (x, +∞) to the same open interval in the extended real numbers.
|
EReal.preimage_coe_Ioi_bot
theorem EReal.preimage_coe_Ioi_bot : Real.toEReal ⁻¹' Set.Ioi ⊥ = Set.univ
This theorem states that the preimage through the canonical inclusion map from real numbers to extended real numbers of the left-open right-infinite interval starting at the bottom (negative infinity) is the universal set of real numbers. In other words, every real number is mapped to an extended real number greater than negative infinity.
More concisely: The canonical inclusion map from the real numbers to extended real numbers maps every real number to an extended real number greater than negative infinity.
|
EReal.range_coe_ennreal
theorem EReal.range_coe_ennreal : Set.range ENNReal.toEReal = Set.Ici 0
This theorem states that the range of the function `ENNReal.toEReal`, which maps nonnegative extended real numbers to extended real numbers, is the set of all extended real numbers that are greater than or equal to zero. In other words, the function `ENNReal.toEReal` maps every nonnegative extended real number to an extended real number, such that the resulting set of values is exactly the set of all extended real numbers that are no less than zero.
More concisely: The range of `ENNReal.toEReal` is the set of extended real numbers greater than or equal to zero.
|
Mathlib.Data.Real.EReal._auxLemma.3
theorem Mathlib.Data.Real.EReal._auxLemma.3 : ∀ {x y : ℝ}, (↑x = ↑y) = (x = y)
This theorem, `Mathlib.Data.Real.EReal._auxLemma.3`, states that for every pair of real numbers `x` and `y`, the property that 'the lifted value of `x` equals the lifted value of `y`' is equivalent to 'x equals y'. In mathematical terms, this is saying if two real numbers are the same when they are embedded into the extended real number system, then they are indeed the same real numbers.
More concisely: The theorem `Mathlib.Data.Real.EReal._auxLemma.3` in Lean 4 asserts that for all real numbers x and y, x = y if and only if their corresponding extended real numbers are equal.
|
EReal.coe_neg
theorem EReal.coe_neg : ∀ (x : ℝ), ↑(-x) = -↑x
This theorem, `EReal.coe_neg`, states that for any real number `x`, the negation of `x` before it is coerced into an extended real number is the same as first coercing `x` into an extended real number and then taking the negation. In mathematical terms, for any real number `x`, `-(x)` and `-x` are identical even after they are converted from real numbers to extended real numbers.
More concisely: For any real number `x`, the negation of its extended real number representation is equivalent to the extended real number representation of `-x`.
|
EReal.coe_mul_bot_of_neg
theorem EReal.coe_mul_bot_of_neg : ∀ {x : ℝ}, x < 0 → ↑x * ⊥ = ⊤
This theorem states that for every real number 'x' such that 'x' is less than zero, the product of the extended real number representation of 'x' and negative infinity equals positive infinity. In other words, if you have a negative real number and you multiply it with negative infinity (in the extended real number system), you will get positive infinity.
More concisely: For every real number `x` below zero, `x * (-∞) = ∞`.
|
Mathlib.Data.Real.EReal._auxLemma.9
theorem Mathlib.Data.Real.EReal._auxLemma.9 : ∀ (x : ℝ), (↑x = ⊤) = False
This theorem, `Mathlib.Data.Real.EReal._auxLemma.9`, asserts that for any real number `x`, the statement that `x` equals positive infinity (`⊤`) is false. In more mathematical terms, no real number can be equal to positive infinity.
More concisely: There exists no real number equal to positive infinity.
|
EReal.neg_le_of_neg_le
theorem EReal.neg_le_of_neg_le : ∀ {a b : EReal}, -a ≤ b → -b ≤ a
This theorem states that for any two extended real numbers `a` and `b`, if the negation of `a` is less than or equal to `b`, then the negation of `b` is less than or equal to `a`. In other words, in the extended real number system, which includes negative infinity and positive infinity along with the standard real numbers, the inequality `-a ≤ b` implies `-b ≤ a`.
More concisely: In the extended real numbers, if `-a ≤ b`, then `-b ≤ a`.
|