Mathlib.Data.EReal.Basic

EReal definition

Full source

/-- The type of extended real numbers `[-∞, ∞]`, constructed as `WithBot (WithTop ℝ)`. -/
def EReal := WithBot (WithTop ℝ)
  deriving Bot, Zero, One, Nontrivial, AddMonoid, PartialOrder, AddCommMonoid

Extended real numbers

Informal description

The type of extended real numbers, denoted as $\overline{\mathbb{R}}$, is defined as the set of real numbers $\mathbb{R}$ augmented with a top element $\infty$ and a bottom element $-\infty$, constructed formally as $\text{WithBot}(\text{WithTop} \mathbb{R})$.

instZeroLEOneClassEReal instance

: ZeroLEOneClass EReal

Full source

instance : ZeroLEOneClass EReal := inferInstanceAs (ZeroLEOneClass (WithBot (WithTop ℝ)))

The Inequality $0 \leq 1$ in Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ satisfy $0 \leq 1$, where $0$ and $1$ are the zero and one elements of $\overline{\mathbb{R}}$ respectively.

instSupSetEReal instance

: SupSet EReal

Full source

instance : SupSet EReal := inferInstanceAs (SupSet (WithBot (WithTop ℝ)))

Supremum Operation on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ are equipped with a supremum operation, which extends the usual supremum operation on $\mathbb{R}$ to handle subsets that may include $\infty$ or $-\infty$.

instInfSetEReal instance

: InfSet EReal

Full source

instance : InfSet EReal := inferInstanceAs (InfSet (WithBot (WithTop ℝ)))

Infimum Operation on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ are equipped with an infimum operation, which extends the usual infimum operation on $\mathbb{R}$ to handle subsets that may include $\infty$ or $-\infty$.

instCompleteLinearOrderEReal instance

: CompleteLinearOrder EReal

Full source

instance : CompleteLinearOrder EReal :=
  inferInstanceAs (CompleteLinearOrder (WithBot (WithTop ℝ)))

Complete Linear Order Structure on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form a complete linear order, where every subset has both a supremum and an infimum. This structure extends the usual order on $\mathbb{R}$ by including $\infty$ as the top element and $-\infty$ as the bottom element.

instLinearOrderEReal instance

: LinearOrder EReal

Full source

instance : LinearOrder EReal :=
  inferInstanceAs (LinearOrder (WithBot (WithTop ℝ)))

Linear Order Structure on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form a linear order, where the order is extended from the usual order on $\mathbb{R}$ with $-\infty$ as the bottom element and $\infty$ as the top element.

instIsOrderedAddMonoidEReal instance

: IsOrderedAddMonoid EReal

Full source

instance : IsOrderedAddMonoid EReal :=
  inferInstanceAs (IsOrderedAddMonoid (WithBot (WithTop ℝ)))

Extended Real Numbers as an Ordered Additive Monoid

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form an ordered additive monoid, where addition is monotone with respect to the order. That is, for any elements $a, b, c \in \overline{\mathbb{R}}$, if $a \leq b$ then $a + c \leq b + c$ and $c + a \leq c + b$.

instAddCommMonoidWithOneEReal instance

: AddCommMonoidWithOne EReal

Full source

instance : AddCommMonoidWithOne EReal :=
  inferInstanceAs (AddCommMonoidWithOne (WithBot (WithTop ℝ)))

Additive Commutative Monoid with One Structure on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form an additive commutative monoid with one, where addition is commutative and there is a distinguished element $1$ serving as the multiplicative identity.

instDenselyOrderedEReal instance

: DenselyOrdered EReal

Full source

instance : DenselyOrdered EReal :=
  inferInstanceAs (DenselyOrdered (WithBot (WithTop ℝ)))

Dense Ordering of Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ are densely ordered, meaning that for any two elements $x < y$ in $\overline{\mathbb{R}}$, there exists an element $z$ such that $x < z < y$.

instCharZeroEReal instance

: CharZero EReal

Full source

instance : CharZero EReal := inferInstanceAs (CharZero (WithBot (WithTop ℝ)))

Characteristic Zero Property of Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ have characteristic zero, meaning the canonical map from the natural numbers $\mathbb{N}$ to $\overline{\mathbb{R}}$ is injective.

Real.toEReal definition

: ℝ → EReal

Full source

/-- The canonical inclusion from reals to ereals. Registered as a coercion. -/
@[coe] def Real.toEReal : ℝ → EReal := WithBot.someWithBot.some ∘ WithTop.some

Inclusion of reals into extended reals

Informal description

The canonical inclusion function from the real numbers $\mathbb{R}$ to the extended real numbers $\overline{\mathbb{R}}$, which maps each real number $x$ to the corresponding element in $\overline{\mathbb{R}}$. This function is registered as a coercion.

EReal.decidableLT instance

: DecidableLT EReal

Full source

instance decidableLT : DecidableLT EReal :=
  WithBot.decidableLT

Decidable Strict Order on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ have a decidable strict order relation $<$.

EReal.instTop instance

: Top EReal

Full source

instance : Top EReal := ⟨WithBot.some ⊤⟩

Existence of Top Element in Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ have a top element $\infty$.

EReal.instCoeReal instance

: Coe ℝ EReal

Full source

instance : Coe ℝ EReal := ⟨Real.toEReal⟩

Canonical Inclusion of Reals into Extended Reals

Informal description

The extended real numbers $\overline{\mathbb{R}}$ have a canonical inclusion from the real numbers $\mathbb{R}$, where each real number $x$ is mapped to the corresponding element in $\overline{\mathbb{R}}$.

EReal.coe_strictMono theorem

: StrictMono Real.toEReal

Full source

theorem coe_strictMono : StrictMono Real.toEReal :=
  WithBot.coe_strictMono.comp WithTop.coe_strictMono

Strict Monotonicity of the Real-to-EReal Inclusion

Informal description

The canonical inclusion function from the real numbers to the extended real numbers, $f : \mathbb{R} \to \overline{\mathbb{R}}$ defined by $f(x) = x$, is strictly monotone. That is, for any real numbers $x$ and $y$, if $x < y$ then $f(x) < f(y)$ in $\overline{\mathbb{R}}$.

EReal.coe_injective theorem

: Injective Real.toEReal

Full source

theorem coe_injective : Injective Real.toEReal :=
  coe_strictMono.injective

Injectivity of the Real-to-EReal Inclusion

Informal description

The canonical inclusion function from the real numbers to the extended real numbers, $f : \mathbb{R} \to \overline{\mathbb{R}}$ defined by $f(x) = x$, is injective. That is, for any real numbers $x$ and $y$, if $f(x) = f(y)$ in $\overline{\mathbb{R}}$, then $x = y$ in $\mathbb{R}$.

EReal.coe_le_coe_iff theorem

{x y : ℝ} : (x : EReal) ≤ (y : EReal) ↔ x ≤ y

Full source

@[simp, norm_cast]
protected theorem coe_le_coe_iff {x y : ℝ} : (x : EReal) ≤ (y : EReal) ↔ x ≤ y :=
  coe_strictMono.le_iff_le

Preservation of Inequality under Real-to-EReal Inclusion

Informal description

For any real numbers $x$ and $y$, the inequality $x \leq y$ holds in the extended real numbers $\overline{\mathbb{R}}$ if and only if $x \leq y$ holds in $\mathbb{R}$.

EReal.coe_lt_coe_iff theorem

{x y : ℝ} : (x : EReal) < (y : EReal) ↔ x < y

Full source

@[simp, norm_cast]
protected theorem coe_lt_coe_iff {x y : ℝ} : (x : EReal) < (y : EReal) ↔ x < y :=
  coe_strictMono.lt_iff_lt

Preservation of Strict Inequality under Real-to-EReal Inclusion

Informal description

For any real numbers $x$ and $y$, the inequality $x < y$ holds in the extended real numbers $\overline{\mathbb{R}}$ if and only if $x < y$ holds in $\mathbb{R}$.

EReal.coe_eq_coe_iff theorem

{x y : ℝ} : (x : EReal) = (y : EReal) ↔ x = y

Full source

@[simp, norm_cast]
protected theorem coe_eq_coe_iff {x y : ℝ} : (x : EReal) = (y : EReal) ↔ x = y :=
  coe_injective.eq_iff

Equality Preservation in Extended Real Numbers

Informal description

For any real numbers $x$ and $y$, the equality $x = y$ holds in the extended real numbers $\overline{\mathbb{R}}$ if and only if $x = y$ holds in $\mathbb{R}$.

EReal.coe_ne_coe_iff theorem

{x y : ℝ} : (x : EReal) ≠ (y : EReal) ↔ x ≠ y

Full source

protected theorem coe_ne_coe_iff {x y : ℝ} : (x : EReal) ≠ (y : EReal)(x : EReal) ≠ (y : EReal) ↔ x ≠ y :=
  coe_injective.ne_iff

Inequality Preservation in Extended Real Numbers: $(x : \overline{\mathbb{R}}) \neq (y : \overline{\mathbb{R}}) \leftrightarrow x \neq y$

Informal description

For any real numbers $x$ and $y$, the inequality $(x : \overline{\mathbb{R}}) \neq (y : \overline{\mathbb{R}})$ holds in the extended real numbers if and only if $x \neq y$ holds in $\mathbb{R}$.

ENNReal.toEReal definition

: ℝ≥0∞ → EReal

Full source

/-- The canonical map from nonnegative extended reals to extended reals. -/
@[coe] def _root_.ENNReal.toEReal : ℝ≥0∞ → EReal
  | ⊤ => ⊤
  | .some x => x.1

Inclusion of extended nonnegative reals into extended reals

Informal description

The function maps an extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ to the corresponding extended real number in $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$. Specifically: - The top element $\infty$ is mapped to $\infty$ in $\overline{\mathbb{R}}$. - For a finite nonnegative real number $x \in \mathbb{R}_{\geq 0}$, it is mapped to the same value $x$ in $\overline{\mathbb{R}}$.

EReal.hasCoeENNReal instance

: Coe ℝ≥0∞ EReal

Full source

instance hasCoeENNReal : Coe ℝ≥0∞ EReal :=
  ⟨ENNReal.toEReal⟩

Inclusion of Extended Nonnegative Reals into Extended Reals

Informal description

There is a canonical inclusion of the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ into the extended real numbers $\overline{\mathbb{R}} = \mathbb{R} \cup \{-\infty, \infty\}$.

EReal.instInhabited instance

: Inhabited EReal

Full source

instance : Inhabited EReal := ⟨0⟩

Inhabited Structure of Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form an inhabited type, meaning there exists a default element in $\overline{\mathbb{R}}$.

EReal.coe_zero theorem

: ((0 : ℝ) : EReal) = 0

Full source

@[simp, norm_cast]
theorem coe_zero : ((0 : ℝ) : EReal) = 0 := rfl

Inclusion of Zero in Extended Reals: $(0 : \mathbb{R}) = 0$

Informal description

The canonical inclusion of the real number $0$ into the extended real numbers $\overline{\mathbb{R}}$ is equal to $0$ in $\overline{\mathbb{R}}$, i.e., $(0 : \mathbb{R}) = 0$ in $\overline{\mathbb{R}}$.

EReal.coe_one theorem

: ((1 : ℝ) : EReal) = 1

Full source

@[simp, norm_cast]
theorem coe_one : ((1 : ℝ) : EReal) = 1 := rfl

Inclusion of One in Extended Reals: $(1 : \mathbb{R}) = 1$

Informal description

The canonical inclusion of the real number $1$ into the extended real numbers $\overline{\mathbb{R}}$ is equal to $1$ in $\overline{\mathbb{R}}$, i.e., $(1 : \mathbb{R}) = 1$ in $\overline{\mathbb{R}}$.

EReal.rec definition

 {motive : EReal → Sort*} (bot : motive ⊥) (coe : ∀ a : ℝ, motive a) (top : motive ⊤) : ∀ a : EReal, motive a

Full source

/-- A recursor for `EReal` in terms of the coercion.

When working in term mode, note that pattern matching can be used directly. -/
@[elab_as_elim, induction_eliminator, cases_eliminator]
protected def rec {motive : EReal → Sort*}
    (bot : motive ⊥) (coe : ∀ a : ℝ, motive a) (top : motive ⊤) : ∀ a : EReal, motive a
  | ⊥ => bot
  | (a : ℝ) => coe a
  | ⊤ => top

Recursor for extended real numbers

Informal description

The recursor for extended real numbers, which allows defining a function on $\overline{\mathbb{R}}$ by specifying its values on $-\infty$, $\infty$, and all real numbers $x \in \mathbb{R}$. Given: - A type family `motive : EReal → Sort*` - A term `bot : motive ⊥` for the bottom element $-\infty$ - A function `coe : ∀ a : ℝ, motive a` for real numbers - A term `top : motive ⊤` for the top element $\infty$ The recursor produces a function `∀ a : EReal, motive a` that: - Maps $-\infty$ to `bot` - Maps any real number $x$ to `coe x` - Maps $\infty$ to `top`

EReal.forall theorem

{p : EReal → Prop} : (∀ r, p r) ↔ p ⊥ ∧ p ⊤ ∧ ∀ r : ℝ, p r

Full source

protected lemma «forall» {p : EReal → Prop} : (∀ r, p r) ↔ p ⊥ ∧ p ⊤ ∧ ∀ r : ℝ, p r where
  mp h := ⟨h _, h _, fun _ ↦ h _⟩
  mpr h := EReal.rec h.1 h.2.2 h.2.1

Universal Quantification Characterization for Extended Reals: $\forall r \in \overline{\mathbb{R}}, p(r) \leftrightarrow p(-\infty) \land p(+\infty) \land \forall r \in \mathbb{R}, p(r)$

Informal description

For any predicate $p$ on the extended real numbers $\overline{\mathbb{R}}$, the universal quantification $\forall r \in \overline{\mathbb{R}}, p(r)$ holds if and only if $p$ holds at $-\infty$, at $+\infty$, and for all real numbers $r \in \mathbb{R}$.

EReal.exists theorem

{p : EReal → Prop} : (∃ r, p r) ↔ p ⊥ ∨ p ⊤ ∨ ∃ r : ℝ, p r

Full source

protected lemma «exists» {p : EReal → Prop} : (∃ r, p r) ↔ p ⊥ ∨ p ⊤ ∨ ∃ r : ℝ, p r where
  mp := by rintro ⟨r, hr⟩; cases r <;> aesop
  mpr := by rintro (h | h | ⟨r, hr⟩) <;> exact ⟨_, ‹_›⟩

Existential Quantification Characterization for Extended Reals: $\exists r \in \overline{\mathbb{R}}, p(r) \leftrightarrow p(-\infty) \lor p(+\infty) \lor \exists r \in \mathbb{R}, p(r)$

Informal description

For any predicate $p$ on the extended real numbers $\overline{\mathbb{R}}$, there exists an element $r \in \overline{\mathbb{R}}$ satisfying $p(r)$ if and only if $p$ holds at $-\infty$, or at $+\infty$, or there exists a real number $r \in \mathbb{R}$ such that $p(r)$ holds.

EReal.mul definition

: EReal → EReal → EReal

Full source

/-- The multiplication on `EReal`. Our definition satisfies `0 * x = x * 0 = 0` for any `x`, and
picks the only sensible value elsewhere. -/
protected def mul : EReal → EReal → EReal
  | ⊥, ⊥ => ⊤
  | ⊥, ⊤ => ⊥
  | ⊥, (y : ℝ) => if 0 < y then ⊥ else if y = 0 then 0 else ⊤
  | ⊤, ⊥ => ⊥
  | ⊤, ⊤ => ⊤
  | ⊤, (y : ℝ) => if 0 < y then ⊤ else if y = 0 then 0 else ⊥
  | (x : ℝ), ⊤ => if 0 < x then ⊤ else if x = 0 then 0 else ⊥
  | (x : ℝ), ⊥ => if 0 < x then ⊥ else if x = 0 then 0 else ⊤
  | (x : ℝ), (y : ℝ) => (x * y : ℝ)

Multiplication on extended real numbers

Informal description

The multiplication operation on extended real numbers $\overline{\mathbb{R}}$ is defined as follows: - $\bot \times \bot = \top$ - $\bot \times \top = \bot$ - For $\bot \times y$ where $y \in \mathbb{R}$: - If $0 < y$ then $\bot \times y = \bot$ - If $y = 0$ then $\bot \times 0 = 0$ - Otherwise $\bot \times y = \top$ - $\top \times \bot = \bot$ - $\top \times \top = \top$ - For $\top \times y$ where $y \in \mathbb{R}$: - If $0 < y$ then $\top \times y = \top$ - If $y = 0$ then $\top \times 0 = 0$ - Otherwise $\top \times y = \bot$ - For $x \in \mathbb{R} \times \top$: - If $0 < x$ then $x \times \top = \top$ - If $x = 0$ then $0 \times \top = 0$ - Otherwise $x \times \top = \bot$ - For $x \in \mathbb{R} \times \bot$: - If $0 < x$ then $x \times \bot = \bot$ - If $x = 0$ then $0 \times \bot = 0$ - Otherwise $x \times \bot = \top$ - For $x, y \in \mathbb{R}$, $x \times y$ is defined as the standard real multiplication. This definition ensures that $0 \times x = x \times 0 = 0$ holds for any $x \in \overline{\mathbb{R}}$.

EReal.instMul instance

: Mul EReal

Full source

instance : Mul EReal := ⟨EReal.mul⟩

Multiplication Structure on Extended Real Numbers

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form a multiplicative structure, where multiplication is defined as follows: - For $x, y \in \mathbb{R}$, multiplication is the standard real multiplication. - For $x = \infty$ or $x = -\infty$ and $y \in \mathbb{R}$ (or vice versa), multiplication follows the rules of extended arithmetic (e.g., $\infty \times y = \infty$ if $y > 0$, $-\infty$ if $y < 0$, and $0$ if $y = 0$). - For $x = \infty$ and $y = -\infty$ (or vice versa), the product is $-\infty$. - For $x = \infty$ and $y = \infty$, the product is $\infty$. - For $x = -\infty$ and $y = -\infty$, the product is $\infty$.

EReal.coe_mul theorem

(x y : ℝ) : (↑(x * y) : EReal) = x * y

Full source

@[simp, norm_cast]
theorem coe_mul (x y : ℝ) : (↑(x * y) : EReal) = x * y :=
  rfl

Preservation of Multiplication under Real-to-EReal Inclusion

Informal description

For any real numbers $x$ and $y$, the canonical inclusion of their product into the extended real numbers equals the product of their inclusions, i.e., $\overline{x \cdot y} = \overline{x} \cdot \overline{y}$ where $\overline{\cdot}$ denotes the inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$.

EReal.induction₂ theorem

 {P : EReal → EReal → Prop} (top_top : P ⊤ ⊤) (top_pos : ∀ x : ℝ, 0 < x → P ⊤ x) (top_zero : P ⊤ 0)
  (top_neg : ∀ x : ℝ, x < 0 → P ⊤ x) (top_bot : P ⊤ ⊥) (pos_top : ∀ x : ℝ, 0 < x → P x ⊤)
  (pos_bot : ∀ x : ℝ, 0 < x → P x ⊥) (zero_top : P 0 ⊤) (coe_coe : ∀ x y : ℝ, P x y) (zero_bot : P 0 ⊥)
  (neg_top : ∀ x : ℝ, x < 0 → P x ⊤) (neg_bot : ∀ x : ℝ, x < 0 → P x ⊥) (bot_top : P ⊥ ⊤)
  (bot_pos : ∀ x : ℝ, 0 < x → P ⊥ x) (bot_zero : P ⊥ 0) (bot_neg : ∀ x : ℝ, x < 0 → P ⊥ x) (bot_bot : P ⊥ ⊥) :
  ∀ x y, P x y

Full source

/-- Induct on two `EReal`s by performing case splits on the sign of one whenever the other is
infinite. -/
@[elab_as_elim]
theorem induction₂ {P : EReal → EReal → Prop} (top_top : P ⊤ ⊤) (top_pos : ∀ x : ℝ, 0 < x → P ⊤ x)
    (top_zero : P ⊤ 0) (top_neg : ∀ x : ℝ, x < 0 → P ⊤ x) (top_bot : P ⊤ ⊥)
    (pos_top : ∀ x : ℝ, 0 < x → P x ⊤) (pos_bot : ∀ x : ℝ, 0 < x → P x ⊥) (zero_top : P 0 ⊤)
    (coe_coe : ∀ x y : ℝ, P x y) (zero_bot : P 0 ⊥) (neg_top : ∀ x : ℝ, x < 0 → P x ⊤)
    (neg_bot : ∀ x : ℝ, x < 0 → P x ⊥) (bot_top : P ⊥ ⊤) (bot_pos : ∀ x : ℝ, 0 < x → P ⊥ x)
    (bot_zero : P ⊥ 0) (bot_neg : ∀ x : ℝ, x < 0 → P ⊥ x) (bot_bot : P ⊥ ⊥) : ∀ x y, P x y
  | ⊥, ⊥ => bot_bot
  | ⊥, (y : ℝ) => by
    rcases lt_trichotomy y 0 with (hy | rfl | hy)
    exacts [bot_neg y hy, bot_zero, bot_pos y hy]
  | ⊥, ⊤ => bot_top
  | (x : ℝ), ⊥ => by
    rcases lt_trichotomy x 0 with (hx | rfl | hx)
    exacts [neg_bot x hx, zero_bot, pos_bot x hx]
  | (x : ℝ), (y : ℝ) => coe_coe _ _
  | (x : ℝ), ⊤ => by
    rcases lt_trichotomy x 0 with (hx | rfl | hx)
    exacts [neg_top x hx, zero_top, pos_top x hx]
  | ⊤, ⊥ => top_bot
  | ⊤, (y : ℝ) => by
    rcases lt_trichotomy y 0 with (hy | rfl | hy)
    exacts [top_neg y hy, top_zero, top_pos y hy]
  | ⊤, ⊤ => top_top

Double Induction Principle for Extended Real Numbers

Informal description

Let $P : \overline{\mathbb{R}} \to \overline{\mathbb{R}} \to \mathrm{Prop}$ be a property of pairs of extended real numbers. To prove that $P(x, y)$ holds for all $x, y \in \overline{\mathbb{R}}$, it suffices to verify the following cases: 1. $P(\infty, \infty)$ 2. For all $x \in \mathbb{R}$ with $0 < x$, $P(\infty, x)$ 3. $P(\infty, 0)$ 4. For all $x \in \mathbb{R}$ with $x < 0$, $P(\infty, x)$ 5. $P(\infty, -\infty)$ 6. For all $x \in \mathbb{R}$ with $0 < x$, $P(x, \infty)$ 7. For all $x \in \mathbb{R}$ with $0 < x$, $P(x, -\infty)$ 8. $P(0, \infty)$ 9. For all $x, y \in \mathbb{R}$, $P(x, y)$ 10. $P(0, -\infty)$ 11. For all $x \in \mathbb{R}$ with $x < 0$, $P(x, \infty)$ 12. For all $x \in \mathbb{R}$ with $x < 0$, $P(x, -\infty)$ 13. $P(-\infty, \infty)$ 14. For all $x \in \mathbb{R}$ with $0 < x$, $P(-\infty, x)$ 15. $P(-\infty, 0)$ 16. For all $x \in \mathbb{R}$ with $x < 0$, $P(-\infty, x)$ 17. $P(-\infty, -\infty)$

EReal.induction₂_symm theorem

 {P : EReal → EReal → Prop} (symm : ∀ {x y}, P x y → P y x) (top_top : P ⊤ ⊤) (top_pos : ∀ x : ℝ, 0 < x → P ⊤ x)
  (top_zero : P ⊤ 0) (top_neg : ∀ x : ℝ, x < 0 → P ⊤ x) (top_bot : P ⊤ ⊥) (pos_bot : ∀ x : ℝ, 0 < x → P x ⊥)
  (coe_coe : ∀ x y : ℝ, P x y) (zero_bot : P 0 ⊥) (neg_bot : ∀ x : ℝ, x < 0 → P x ⊥) (bot_bot : P ⊥ ⊥) : ∀ x y, P x y

Full source

/-- Induct on two `EReal`s by performing case splits on the sign of one whenever the other is
infinite. This version eliminates some cases by assuming that the relation is symmetric. -/
@[elab_as_elim]
theorem induction₂_symm {P : EReal → EReal → Prop} (symm : ∀ {x y}, P x y → P y x)
    (top_top : P ⊤ ⊤) (top_pos : ∀ x : ℝ, 0 < x → P ⊤ x) (top_zero : P ⊤ 0)
    (top_neg : ∀ x : ℝ, x < 0 → P ⊤ x) (top_bot : P ⊤ ⊥) (pos_bot : ∀ x : ℝ, 0 < x → P x ⊥)
    (coe_coe : ∀ x y : ℝ, P x y) (zero_bot : P 0 ⊥) (neg_bot : ∀ x : ℝ, x < 0 → P x ⊥)
    (bot_bot : P ⊥ ⊥) : ∀ x y, P x y :=
  @induction₂ P top_top top_pos top_zero top_neg top_bot (fun _ h => symm <| top_pos _ h)
    pos_bot (symm top_zero) coe_coe zero_bot (fun _ h => symm <| top_neg _ h) neg_bot (symm top_bot)
    (fun _ h => symm <| pos_bot _ h) (symm zero_bot) (fun _ h => symm <| neg_bot _ h) bot_bot

Symmetric Double Induction Principle for Extended Real Numbers

Informal description

Let $P : \overline{\mathbb{R}} \to \overline{\mathbb{R}} \to \mathrm{Prop}$ be a symmetric property (i.e., $P(x,y) \Rightarrow P(y,x)$ for all $x,y \in \overline{\mathbb{R}}$). To prove that $P(x,y)$ holds for all $x,y \in \overline{\mathbb{R}}$, it suffices to verify the following cases: 1. $P(\infty, \infty)$ 2. For all $x \in \mathbb{R}$ with $0 < x$, $P(\infty, x)$ 3. $P(\infty, 0)$ 4. For all $x \in \mathbb{R}$ with $x < 0$, $P(\infty, x)$ 5. $P(\infty, -\infty)$ 6. For all $x \in \mathbb{R}$ with $0 < x$, $P(x, -\infty)$ 7. For all $x, y \in \mathbb{R}$, $P(x, y)$ 8. $P(0, -\infty)$ 9. For all $x \in \mathbb{R}$ with $x < 0$, $P(x, -\infty)$ 10. $P(-\infty, -\infty)$

EReal.mul_comm theorem

(x y : EReal) : x * y = y * x

Full source

protected theorem mul_comm (x y : EReal) : x * y = y * x := by
  induction x <;> induction y  <;>
    try { rfl }
  rw [← coe_mul, ← coe_mul, mul_comm]

Commutativity of Multiplication in Extended Real Numbers: $x \cdot y = y \cdot x$

Informal description

For any extended real numbers $x, y \in \overline{\mathbb{R}}$, the multiplication operation is commutative, i.e., $x \cdot y = y \cdot x$.

EReal.one_mul theorem

: ∀ x : EReal, 1 * x = x

Full source

protected theorem one_mul : ∀ x : EReal, 1 * x = x
  | ⊤ => if_pos one_pos
  | ⊥ => if_pos one_pos
  | (x : ℝ) => congr_arg Real.toEReal (one_mul x)

Multiplicative Identity Property in Extended Real Numbers: $1 \cdot x = x$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the product of $1$ and $x$ is equal to $x$, i.e., $1 \cdot x = x$.

EReal.zero_mul theorem

: ∀ x : EReal, 0 * x = 0

Full source

protected theorem zero_mul : ∀ x : EReal, 0 * x = 0
  | ⊤ => (if_neg (lt_irrefl _)).trans (if_pos rfl)
  | ⊥ => (if_neg (lt_irrefl _)).trans (if_pos rfl)
  | (x : ℝ) => congr_arg Real.toEReal (zero_mul x)

Multiplication by Zero in Extended Real Numbers: $0 \cdot x = 0$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the product of $0$ and $x$ is $0$, i.e., $0 \cdot x = 0$.

EReal.instMulZeroOneClass instance

: MulZeroOneClass EReal

Full source

instance : MulZeroOneClass EReal where
  one_mul := EReal.one_mul
  mul_one := fun x => by rw [EReal.mul_comm, EReal.one_mul]
  zero_mul := EReal.zero_mul
  mul_zero := fun x => by rw [EReal.mul_comm, EReal.zero_mul]

Extended Real Numbers as a MulZeroOneClass Structure

Informal description

The extended real numbers $\overline{\mathbb{R}}$ form a multiplicative structure with zero and one, where: 1. $1$ is a multiplicative identity (i.e., $1 \cdot x = x$ for all $x \in \overline{\mathbb{R}}$) 2. $0$ is an absorbing element (i.e., $0 \cdot x = 0$ for all $x \in \overline{\mathbb{R}}$)

EReal.canLift instance

: CanLift EReal ℝ (↑) fun r => r ≠ ⊤ ∧ r ≠ ⊥

Full source

instance canLift : CanLift EReal ℝ (↑) fun r => r ≠ ⊤r ≠ ⊤ ∧ r ≠ ⊥ where
  prf x hx := by
    induction x
    · simp at hx
    · simp
    · simp at hx

Lifting Condition from Extended Reals to Reals

Informal description

The extended real numbers $\overline{\mathbb{R}}$ can be lifted to real numbers $\mathbb{R}$ via the canonical inclusion map, provided the element is neither $\top$ (positive infinity) nor $\bot$ (negative infinity).

EReal.toReal definition

: EReal → ℝ

Full source

/-- The map from extended reals to reals sending infinities to zero. -/
def toReal : EReal → ℝ
  | ⊥ => 0
  | ⊤ => 0
  | (x : ℝ) => x

Extended real to real conversion (infinities to zero)

Informal description

The function maps an extended real number $x \in \overline{\mathbb{R}}$ to a real number as follows: if $x$ is $\top$ (positive infinity) or $\bot$ (negative infinity), it returns $0$; if $x$ is a real number, it returns $x$ itself.

EReal.toReal_top theorem

: toReal ⊤ = 0

Full source

@[simp]
theorem toReal_top : toReal ⊤ = 0 :=
  rfl

Conversion of Positive Infinity to Zero in Extended Reals

Informal description

The extended real to real conversion function maps the top element $\top$ (positive infinity) to $0$, i.e., $\text{toReal}(\top) = 0$.

EReal.toReal_bot theorem

: toReal ⊥ = 0

Full source

@[simp]
theorem toReal_bot : toReal ⊥ = 0 :=
  rfl

Conversion of Negative Infinity to Zero in Extended Reals

Informal description

The extended real to real conversion function maps the bottom element $\bot$ (negative infinity) to $0$, i.e., $\text{toReal}(\bot) = 0$.

EReal.toReal_zero theorem

: toReal 0 = 0

Full source

@[simp]
theorem toReal_zero : toReal 0 = 0 :=
  rfl

Extended Real Zero Conversion: $\text{toReal}(0) = 0$

Informal description

The extended real to real conversion function maps the extended real number $0$ to the real number $0$, i.e., $\text{toReal}(0) = 0$.

EReal.toReal_one theorem

: toReal 1 = 1

Full source

@[simp]
theorem toReal_one : toReal 1 = 1 :=
  rfl

Extended Real One Conversion: $\text{toReal}(1) = 1$

Informal description

The extended real to real conversion function maps the extended real number $1$ to the real number $1$, i.e., $\text{toReal}(1) = 1$.

EReal.toReal_coe theorem

(x : ℝ) : toReal (x : EReal) = x

Full source

@[simp]
theorem toReal_coe (x : ℝ) : toReal (x : EReal) = x :=
  rfl

Extended Real to Real Conversion Preserves Real Numbers: $\text{toReal}(x) = x$

Informal description

For any real number $x$, the extended real to real conversion function maps the extended real number obtained by including $x$ into the extended reals back to $x$ itself, i.e., $\text{toReal}(x) = x$.

EReal.bot_lt_coe theorem

(x : ℝ) : (⊥ : EReal) < x

Full source

@[simp]
theorem bot_lt_coe (x : ℝ) : (⊥ : EReal) < x :=
  WithBot.bot_lt_coe _

Bottom Element is Less Than Any Real in Extended Reals

Informal description

For any real number $x$, the bottom element $-\infty$ of the extended real numbers is strictly less than $x$, i.e., $-\infty < x$.

EReal.coe_ne_bot theorem

(x : ℝ) : (x : EReal) ≠ ⊥

Full source

@[simp]
theorem coe_ne_bot (x : ℝ) : (x : EReal) ≠ ⊥ :=
  (bot_lt_coe x).ne'

Real Numbers Are Not Bottom in Extended Reals

Informal description

For any real number $x$, the extended real number obtained by including $x$ in $\overline{\mathbb{R}}$ is not equal to the bottom element $-\infty$, i.e., $x \neq -\infty$.

EReal.bot_ne_coe theorem

(x : ℝ) : (⊥ : EReal) ≠ x

Full source

@[simp]
theorem bot_ne_coe (x : ℝ) : (⊥ : EReal) ≠ x :=
  (bot_lt_coe x).ne

Bottom Element Not Equal to Any Real in Extended Reals

Informal description

For any real number $x$, the bottom element $-\infty$ of the extended real numbers is not equal to $x$, i.e., $-\infty \neq x$.

EReal.coe_lt_top theorem

(x : ℝ) : (x : EReal) < ⊤

Full source

@[simp]
theorem coe_lt_top (x : ℝ) : (x : EReal) < ⊤ :=
  WithBot.coe_lt_coe.2 <| WithTop.coe_lt_top _

Real Numbers are Strictly Below Infinity in Extended Reals

Informal description

For any real number $x$, the extended real number obtained by including $x$ in $\overline{\mathbb{R}}$ is strictly less than the top element $\infty$, i.e., $x < \infty$.

EReal.coe_ne_top theorem

(x : ℝ) : (x : EReal) ≠ ⊤

Full source

@[simp]
theorem coe_ne_top (x : ℝ) : (x : EReal) ≠ ⊤ :=
  (coe_lt_top x).ne

Real Numbers are Not Infinity in Extended Reals

Informal description

For any real number $x$, the extended real number obtained by including $x$ in $\overline{\mathbb{R}}$ is not equal to the top element $\infty$, i.e., $x \neq \infty$.

EReal.top_ne_coe theorem

(x : ℝ) : (⊤ : EReal) ≠ x

Full source

@[simp]
theorem top_ne_coe (x : ℝ) : (⊤ : EReal) ≠ x :=
  (coe_lt_top x).ne'

Infinity is not equal to any real number in extended reals

Informal description

For any real number $x$, the top element $\infty$ in the extended real numbers $\overline{\mathbb{R}}$ is not equal to $x$.

EReal.bot_lt_zero theorem

: (⊥ : EReal) < 0

Full source

@[simp]
theorem bot_lt_zero : (⊥ : EReal) < 0 :=
  bot_lt_coe 0

$-\infty < 0$ in extended reals

Informal description

The bottom element $-\infty$ of the extended real numbers is strictly less than $0$, i.e., $-\infty < 0$.

EReal.bot_ne_zero theorem

: (⊥ : EReal) ≠ 0

Full source

@[simp]
theorem bot_ne_zero : (⊥ : EReal) ≠ 0 :=
  (coe_ne_bot 0).symm

$-\infty \neq 0$ in extended reals

Informal description

The bottom element $-\infty$ of the extended real numbers is not equal to $0$.

EReal.zero_ne_bot theorem

: (0 : EReal) ≠ ⊥

Full source

@[simp]
theorem zero_ne_bot : (0 : EReal) ≠ ⊥ :=
  coe_ne_bot 0

Non-Equality of Zero and Negative Infinity in Extended Reals

Informal description

The extended real number obtained by including the real number $0$ in $\overline{\mathbb{R}}$ is not equal to the bottom element $-\infty$, i.e., $0 \neq -\infty$.

EReal.zero_lt_top theorem

: (0 : EReal) < ⊤

Full source

@[simp]
theorem zero_lt_top : (0 : EReal) < ⊤ :=
  coe_lt_top 0

Zero is Strictly Below Infinity in Extended Reals

Informal description

The extended real number obtained by including the real number $0$ in $\overline{\mathbb{R}}$ is strictly less than the top element $\infty$, i.e., $0 < \infty$.

EReal.zero_ne_top theorem

: (0 : EReal) ≠ ⊤

Full source

@[simp]
theorem zero_ne_top : (0 : EReal) ≠ ⊤ :=
  coe_ne_top 0

Non-Equality of Zero and Infinity in Extended Reals

Informal description

The extended real number obtained by including the real number $0$ in $\overline{\mathbb{R}}$ is not equal to the top element $\infty$, i.e., $0 \neq \infty$.

EReal.top_ne_zero theorem

: (⊤ : EReal) ≠ 0

Full source

@[simp]
theorem top_ne_zero : (⊤ : EReal) ≠ 0 :=
  (coe_ne_top 0).symm

Non-Equality of Infinity and Zero in Extended Reals

Informal description

The top element $\infty$ in the extended real numbers $\overline{\mathbb{R}}$ is not equal to the real number $0$, i.e., $\infty \neq 0$.

EReal.range_coe theorem

: range Real.toEReal = {⊥, ⊤}ᶜ

Full source

theorem range_coe : range Real.toEReal = {⊥, ⊤}{⊥, ⊤}ᶜ := by
  ext x
  induction x <;> simp

Range of Real Inclusion in Extended Reals Excludes Infinities

Informal description

The range of the canonical inclusion map from real numbers to extended real numbers is equal to the complement of the set $\{-\infty, \infty\}$, i.e., $\text{range}(\text{Real.toEReal}) = \overline{\mathbb{R}} \setminus \{-\infty, \infty\}$.

EReal.range_coe_eq_Ioo theorem

: range Real.toEReal = Ioo ⊥ ⊤

Full source

theorem range_coe_eq_Ioo : range Real.toEReal = Ioo ⊥ ⊤ := by
  ext x
  induction x <;> simp

Range of Real Inclusion in Extended Reals is Open Interval $(-\infty, \infty)$

Informal description

The range of the canonical inclusion map from the real numbers $\mathbb{R}$ to the extended real numbers $\overline{\mathbb{R}}$ is equal to the open interval $(-\infty, \infty)$ in $\overline{\mathbb{R}}$.

EReal.coe_add theorem

(x y : ℝ) : (↑(x + y) : EReal) = x + y

Full source

@[simp, norm_cast]
theorem coe_add (x y : ℝ) : (↑(x + y) : EReal) = x + y :=
  rfl

Additivity of Real Number Inclusion into Extended Reals

Informal description

For any real numbers $x$ and $y$, the canonical inclusion of their sum $x + y$ into the extended real numbers $\overline{\mathbb{R}}$ is equal to the sum of their inclusions, i.e., $(x + y : \overline{\mathbb{R}}) = (x : \overline{\mathbb{R}}) + (y : \overline{\mathbb{R}})$.

EReal.coe_nsmul theorem

(n : ℕ) (x : ℝ) : (↑(n • x) : EReal) = n • (x : EReal)

Full source

@[norm_cast]
theorem coe_nsmul (n : ℕ) (x : ℝ) : (↑(n • x) : EReal) = n • (x : EReal) :=
  map_nsmul (⟨⟨Real.toEReal, coe_zero⟩, coe_add⟩ : ℝℝ →+ EReal) _ _

Scalar Multiplication Compatibility in Extended Reals: $(n \cdot x : \overline{\mathbb{R}}) = n \cdot (x : \overline{\mathbb{R}})$

Informal description

For any natural number $n$ and real number $x$, the canonical inclusion of the scalar multiple $n \cdot x$ into the extended real numbers $\overline{\mathbb{R}}$ is equal to the scalar multiple of the inclusion of $x$, i.e., $(n \cdot x : \overline{\mathbb{R}}) = n \cdot (x : \overline{\mathbb{R}})$.

EReal.coe_eq_zero theorem

{x : ℝ} : (x : EReal) = 0 ↔ x = 0

Full source

@[simp, norm_cast]
theorem coe_eq_zero {x : ℝ} : (x : EReal) = 0 ↔ x = 0 :=
  EReal.coe_eq_coe_iff

Equivalence of Zero in Extended Reals and Reals

Informal description

For any real number $x$, the canonical inclusion of $x$ in the extended real numbers $\overline{\mathbb{R}}$ equals $0$ if and only if $x = 0$ in $\mathbb{R}$.

EReal.coe_eq_one theorem

{x : ℝ} : (x : EReal) = 1 ↔ x = 1

Full source

@[simp, norm_cast]
theorem coe_eq_one {x : ℝ} : (x : EReal) = 1 ↔ x = 1 :=
  EReal.coe_eq_coe_iff

Extended Real Inclusion Preserves Equality with One: $(x : \overline{\mathbb{R}}) = 1 \leftrightarrow x = 1$

Informal description

For any real number $x$, the extended real number obtained by including $x$ into $\overline{\mathbb{R}}$ is equal to $1$ if and only if $x = 1$ in $\mathbb{R}$.

EReal.coe_ne_zero theorem

{x : ℝ} : (x : EReal) ≠ 0 ↔ x ≠ 0

Full source

theorem coe_ne_zero {x : ℝ} : (x : EReal) ≠ 0(x : EReal) ≠ 0 ↔ x ≠ 0 :=
  EReal.coe_ne_coe_iff

Nonzero Preservation in Extended Reals: $(x : \overline{\mathbb{R}}) \neq 0 \leftrightarrow x \neq 0$

Informal description

For any real number $x$, the extended real number $(x : \overline{\mathbb{R}})$ is not equal to $0$ if and only if $x \neq 0$ in $\mathbb{R}$.

EReal.coe_ne_one theorem

{x : ℝ} : (x : EReal) ≠ 1 ↔ x ≠ 1

Full source

theorem coe_ne_one {x : ℝ} : (x : EReal) ≠ 1(x : EReal) ≠ 1 ↔ x ≠ 1 :=
  EReal.coe_ne_coe_iff

Inequality Preservation for One in Extended Reals: $(x : \overline{\mathbb{R}}) \neq 1 \leftrightarrow x \neq 1$

Informal description

For any real number $x$, the extended real number corresponding to $x$ is not equal to $1$ if and only if $x \neq 1$ in $\mathbb{R}$.

EReal.coe_nonneg theorem

{x : ℝ} : (0 : EReal) ≤ x ↔ 0 ≤ x

Full source

@[simp, norm_cast]
protected theorem coe_nonneg {x : ℝ} : (0 : EReal) ≤ x ↔ 0 ≤ x :=
  EReal.coe_le_coe_iff

Nonnegativity Preservation in Extended Reals

Informal description

For any real number $x$, the inclusion of $x$ in the extended real numbers satisfies $0 \leq x$ if and only if $0 \leq x$ holds in $\mathbb{R}$.

EReal.coe_nonpos theorem

{x : ℝ} : (x : EReal) ≤ 0 ↔ x ≤ 0

Full source

@[simp, norm_cast]
protected theorem coe_nonpos {x : ℝ} : (x : EReal) ≤ 0 ↔ x ≤ 0 :=
  EReal.coe_le_coe_iff

Nonpositivity Preservation in Extended Reals

Informal description

For any real number $x$, the extended real number corresponding to $x$ is less than or equal to $0$ if and only if $x \leq 0$ in $\mathbb{R}$.

EReal.coe_pos theorem

{x : ℝ} : (0 : EReal) < x ↔ 0 < x

Full source

@[simp, norm_cast]
protected theorem coe_pos {x : ℝ} : (0 : EReal) < x ↔ 0 < x :=
  EReal.coe_lt_coe_iff

Positivity Preservation in Extended Reals: $0 < x$ in $\overline{\mathbb{R}}$ iff $0 < x$ in $\mathbb{R}$

Informal description

For any real number $x$, the extended real number $0$ is strictly less than $x$ in $\overline{\mathbb{R}}$ if and only if $0 < x$ in $\mathbb{R}$.

EReal.coe_neg' theorem

{x : ℝ} : (x : EReal) < 0 ↔ x < 0

Full source

@[simp, norm_cast]
protected theorem coe_neg' {x : ℝ} : (x : EReal) < 0 ↔ x < 0 :=
  EReal.coe_lt_coe_iff

Negativity Preservation in Extended Reals

Informal description

For any real number $x$, the extended real number corresponding to $x$ is negative (i.e., $(x : \overline{\mathbb{R}}) < 0$) if and only if $x$ is negative in $\mathbb{R}$ (i.e., $x < 0$).

EReal.toReal_eq_zero_iff theorem

{x : EReal} : x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥

Full source

lemma toReal_eq_zero_iff {x : EReal} : x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x = ⊥ := by
  cases x <;> norm_num

Zero Real Part Criterion for Extended Real Numbers: $\text{toReal}(x) = 0 \leftrightarrow x \in \{0, \top, \bot\}$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the real part of $x$ is zero if and only if $x$ is zero, positive infinity ($\top$), or negative infinity ($\bot$). In other words: $$ \text{toReal}(x) = 0 \leftrightarrow x = 0 \lor x = \top \lor x = \bot $$

EReal.toReal_ne_zero_iff theorem

{x : EReal} : x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥

Full source

lemma toReal_ne_zero_iff {x : EReal} : x.toReal ≠ 0x.toReal ≠ 0 ↔ x ≠ 0 ∧ x ≠ ⊤ ∧ x ≠ ⊥ := by
  simp only [ne_eq, toReal_eq_zero_iff, not_or]

Nonzero Real Part Criterion for Extended Real Numbers

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the real part of $x$ is nonzero if and only if $x$ is neither zero, nor positive infinity ($\top$), nor negative infinity ($\bot$). In other words: $$ \text{toReal}(x) \neq 0 \leftrightarrow x \neq 0 \land x \neq \top \land x \neq \bot $$

EReal.toReal_eq_toReal theorem

 {x y : EReal} (hx_top : x ≠ ⊤) (hx_bot : x ≠ ⊥) (hy_top : y ≠ ⊤) (hy_bot : y ≠ ⊥) : x.toReal = y.toReal ↔ x = y

Full source

lemma toReal_eq_toReal {x y : EReal} (hx_top : x ≠ ⊤) (hx_bot : x ≠ ⊥)
    (hy_top : y ≠ ⊤) (hy_bot : y ≠ ⊥) :
    x.toReal = y.toReal ↔ x = y := by
  lift x to ℝ using ⟨hx_top, hx_bot⟩
  lift y to ℝ using ⟨hy_top, hy_bot⟩
  simp

Equality of Extended Reals via Real Parts

Informal description

For any extended real numbers $x, y \in \overline{\mathbb{R}}$ such that $x$ is neither $\top$ (positive infinity) nor $\bot$ (negative infinity), and $y$ is neither $\top$ nor $\bot$, the real parts of $x$ and $y$ are equal if and only if $x = y$. In other words: $$ \text{toReal}(x) = \text{toReal}(y) \leftrightarrow x = y $$

EReal.toReal_nonneg theorem

{x : EReal} (hx : 0 ≤ x) : 0 ≤ x.toReal

Full source

lemma toReal_nonneg {x : EReal} (hx : 0 ≤ x) : 0 ≤ x.toReal := by
  cases x
  · norm_num
  · exact toReal_coe _ ▸ EReal.coe_nonneg.mp hx
  · norm_num

Nonnegativity of Extended Real to Real Conversion

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, if $0 \leq x$, then the real part of $x$ is nonnegative, i.e., $0 \leq \text{toReal}(x)$.

EReal.toReal_nonpos theorem

{x : EReal} (hx : x ≤ 0) : x.toReal ≤ 0

Full source

lemma toReal_nonpos {x : EReal} (hx : x ≤ 0) : x.toReal ≤ 0 := by
  cases x
  · norm_num
  · exact toReal_coe _ ▸ EReal.coe_nonpos.mp hx
  · norm_num

Nonpositivity Preservation in Extended Real to Real Conversion

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$ such that $x \leq 0$, the real number obtained by applying the `toReal` function to $x$ is less than or equal to $0$.

EReal.toReal_le_toReal theorem

{x y : EReal} (h : x ≤ y) (hx : x ≠ ⊥) (hy : y ≠ ⊤) : x.toReal ≤ y.toReal

Full source

theorem toReal_le_toReal {x y : EReal} (h : x ≤ y) (hx : x ≠ ⊥) (hy : y ≠ ⊤) :
    x.toReal ≤ y.toReal := by
  lift x to ℝ using ⟨ne_top_of_le_ne_top hy h, hx⟩
  lift y to ℝ using ⟨hy, ne_bot_of_le_ne_bot hx h⟩
  simpa using h

Monotonicity of Extended Real to Real Conversion: $x \leq y \Rightarrow \text{toReal}(x) \leq \text{toReal}(y)$ for Finite $x$ and $y$

Informal description

For any extended real numbers $x$ and $y$ such that $x \leq y$, $x \neq -\infty$, and $y \neq +\infty$, the inequality $\text{toReal}(x) \leq \text{toReal}(y)$ holds, where $\text{toReal}$ maps extended reals to reals by sending finite values to themselves and infinite values to $0$.

EReal.coe_toReal theorem

{x : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) : (x.toReal : EReal) = x

Full source

theorem coe_toReal {x : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) : (x.toReal : EReal) = x := by
  lift x to ℝ using ⟨hx, h'x⟩
  rfl

Canonical Inclusion of Extended Real to Real Conversion is Identity on Finite Values

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$ that is neither positive infinity ($\top$) nor negative infinity ($\bot$), the canonical inclusion of the real number obtained by applying the `toReal` function to $x$ equals $x$ itself, i.e., $\overline{x.\text{toReal}} = x$.

EReal.le_coe_toReal theorem

{x : EReal} (h : x ≠ ⊤) : x ≤ x.toReal

Full source

theorem le_coe_toReal {x : EReal} (h : x ≠ ⊤) : x ≤ x.toReal := by
  by_cases h' : x = ⊥
  · simp only [h', bot_le]
  · simp only [le_refl, coe_toReal h h']

Extended Real Number is Bounded Above by its Real Inclusion for Non-Infinite Values

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$ that is not positive infinity ($x \neq \infty$), we have $x \leq \overline{x.\text{toReal}}$, where $\text{toReal}$ maps extended reals to reals by sending finite values to themselves and infinite values to 0, and $\overline{\cdot}$ denotes the canonical inclusion from $\mathbb{R}$ to $\overline{\mathbb{R}}$.

EReal.coe_toReal_le theorem

{x : EReal} (h : x ≠ ⊥) : ↑x.toReal ≤ x

Full source

theorem coe_toReal_le {x : EReal} (h : x ≠ ⊥) : ↑x.toReal ≤ x := by
  by_cases h' : x = ⊤
  · simp only [h', le_top]
  · simp only [le_refl, coe_toReal h' h]

Canonical Inclusion of Extended Real to Real Conversion is Lower Bound for Finite Values

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$ that is not negative infinity ($-\infty$), the canonical inclusion of the real number obtained by applying the `toReal` function to $x$ is less than or equal to $x$, i.e., $\overline{x.\text{toReal}} \leq x$.

EReal.exists_between_coe_real theorem

{x z : EReal} (h : x < z) : ∃ y : ℝ, x < y ∧ y < z

Full source

lemma exists_between_coe_real {x z : EReal} (h : x < z) : ∃ y : ℝ, x < y ∧ y < z := by
  obtain ⟨a, ha₁, ha₂⟩ := exists_between h
  induction a with
  | bot => exact (not_lt_bot ha₁).elim
  | coe a₀ => exact ⟨a₀, ha₁, ha₂⟩
  | top => exact (not_top_lt ha₂).elim

Density of Reals in Extended Reals: $\exists y \in \mathbb{R}, x < y < z$

Informal description

For any extended real numbers $x$ and $z$ such that $x < z$, there exists a real number $y$ satisfying $x < y < z$.

EReal.image_coe_Icc theorem

(x y : ℝ) : Real.toEReal '' Icc x y = Icc ↑x ↑y

Full source

@[simp]
lemma image_coe_Icc (x y : ℝ) : Real.toERealReal.toEReal '' Icc x y = Icc ↑x ↑y := by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Icc, WithBot.image_coe_Icc]
  rfl

Image of Real Closed Interval in Extended Reals Equals Extended Closed Interval

Informal description

For any real numbers $x$ and $y$, the image of the closed interval $[x, y]$ under the canonical inclusion map from $\mathbb{R}$ to $\overline{\mathbb{R}}$ is equal to the closed interval $[x, y]$ in $\overline{\mathbb{R}}$.

EReal.image_coe_Ico theorem

(x y : ℝ) : Real.toEReal '' Ico x y = Ico ↑x ↑y

Full source

@[simp]
lemma image_coe_Ico (x y : ℝ) : Real.toERealReal.toEReal '' Ico x y = Ico ↑x ↑y := by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Ico, WithBot.image_coe_Ico]
  rfl

Image of Real Interval under Inclusion Matches Extended Real Interval

Informal description

For any real numbers $x$ and $y$, the image of the left-closed right-open interval $[x, y)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the left-closed right-open interval $[x, y)$ in the extended real numbers $\overline{\mathbb{R}}$.

EReal.image_coe_Ici theorem

(x : ℝ) : Real.toEReal '' Ici x = Ico ↑x ⊤

Full source

@[simp]
lemma image_coe_Ici (x : ℝ) : Real.toERealReal.toEReal '' Ici x = Ico ↑x ⊤ := by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Ici, WithBot.image_coe_Ico]
  rfl

Image of $[x, \infty)$ under real inclusion equals $[x, \top)$ in extended reals

Informal description

For any real number $x$, the image of the interval $[x, \infty)$ under the canonical inclusion $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the interval $[x, \top)$ in the extended real numbers $\overline{\mathbb{R}}$, where $\top$ denotes the top element.

EReal.image_coe_Ioc theorem

(x y : ℝ) : Real.toEReal '' Ioc x y = Ioc ↑x ↑y

Full source

@[simp]
lemma image_coe_Ioc (x y : ℝ) : Real.toERealReal.toEReal '' Ioc x y = Ioc ↑x ↑y := by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Ioc, WithBot.image_coe_Ioc]
  rfl

Image of Real Interval $(x, y]$ in Extended Reals Equals Extended Interval $(x, y]$

Informal description

For any real numbers $x$ and $y$, the image of the left-open right-closed interval $(x, y] \subseteq \mathbb{R}$ under the canonical inclusion $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the left-open right-closed interval $(x, y]$ in the extended real numbers $\overline{\mathbb{R}}$.

EReal.image_coe_Ioo theorem

(x y : ℝ) : Real.toEReal '' Ioo x y = Ioo ↑x ↑y

Full source

@[simp]
lemma image_coe_Ioo (x y : ℝ) : Real.toERealReal.toEReal '' Ioo x y = Ioo ↑x ↑y := by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Ioo, WithBot.image_coe_Ioo]
  rfl

Image of Real Open Interval in Extended Reals Equals Extended Real Open Interval

Informal description

For any real numbers $x$ and $y$, the image of the open interval $(x, y)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the open interval $(x, y)$ in the extended real numbers $\overline{\mathbb{R}}$.

EReal.image_coe_Ioi theorem

(x : ℝ) : Real.toEReal '' Ioi x = Ioo ↑x ⊤

Full source

@[simp]
lemma image_coe_Ioi (x : ℝ) : Real.toERealReal.toEReal '' Ioi x = Ioo ↑x ⊤ := by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Ioi, WithBot.image_coe_Ioo]
  rfl

Image of Right-Infinite Real Interval in Extended Reals is $(x, \infty)$

Informal description

For any real number $x$, the image of the open right-infinite interval $(x, \infty)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the open interval $(x, \infty)$ in the extended real numbers $\overline{\mathbb{R}}$, where $\infty$ is the top element.

EReal.image_coe_Iic theorem

(x : ℝ) : Real.toEReal '' Iic x = Ioc ⊥ ↑x

Full source

@[simp]
lemma image_coe_Iic (x : ℝ) : Real.toERealReal.toEReal '' Iic x = Ioc ⊥ ↑x := by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Iic, WithBot.image_coe_Iic]
  rfl

Image of $(-\infty, x]$ under real inclusion equals $(-\infty, x]$ in extended reals

Informal description

For any real number $x$, the image of the left-infinite right-closed interval $(-\infty, x]$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the left-open right-closed interval $(-\infty, x]$ in $\overline{\mathbb{R}}$, where the left endpoint is the bottom element $\bot$ (i.e., $-\infty$).

EReal.image_coe_Iio theorem

(x : ℝ) : Real.toEReal '' Iio x = Ioo ⊥ ↑x

Full source

@[simp]
lemma image_coe_Iio (x : ℝ) : Real.toERealReal.toEReal '' Iio x = Ioo ⊥ ↑x := by
  refine (image_comp WithBot.some WithTop.some _).trans ?_
  rw [WithTop.image_coe_Iio, WithBot.image_coe_Iio]
  rfl

Image of $(-\infty, x)$ under real inclusion equals $(-\infty, x)$ in extended reals

Informal description

For any real number $x$, the image of the left-infinite right-open interval $(-\infty, x)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the open interval $(-\infty, x)$ in the extended real numbers $\overline{\mathbb{R}}$, where $-\infty$ is the bottom element of $\overline{\mathbb{R}}$.

EReal.preimage_coe_Ici theorem

(x : ℝ) : Real.toEReal ⁻¹' Ici x = Ici x

Full source

@[simp]
lemma preimage_coe_Ici (x : ℝ) : Real.toERealReal.toEReal ⁻¹' Ici x = Ici x := by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Ici (WithBot.some (WithTop.some x))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Ici, WithTop.preimage_coe_Ici]

Preimage of Extended Left-Closed Interval under Real Inclusion

Informal description

For any real number $x$, the preimage of the extended interval $[x, \infty]$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the interval $[x, \infty)$ in $\mathbb{R}$.

EReal.preimage_coe_Ioi theorem

(x : ℝ) : Real.toEReal ⁻¹' Ioi x = Ioi x

Full source

@[simp]
lemma preimage_coe_Ioi (x : ℝ) : Real.toERealReal.toEReal ⁻¹' Ioi x = Ioi x := by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Ioi (WithBot.some (WithTop.some x))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Ioi, WithTop.preimage_coe_Ioi]

Preimage of Extended Right-Infinite Interval under Real Inclusion

Informal description

For any real number $x$, the preimage of the interval $(x, \infty)$ in the extended real numbers $\overline{\mathbb{R}}$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the interval $(x, \infty)$ in $\mathbb{R}$.

EReal.preimage_coe_Ioi_bot theorem

: Real.toEReal ⁻¹' Ioi ⊥ = univ

Full source

@[simp]
lemma preimage_coe_Ioi_bot : Real.toERealReal.toEReal ⁻¹' Ioi ⊥ = univ := by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Ioi ⊥) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Ioi_bot, preimage_univ]

Preimage of $(\bot, \infty)$ under real inclusion is universal set

Informal description

The preimage of the interval $(\bot, \infty)$ in the extended real numbers $\overline{\mathbb{R}}$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the entire set of real numbers $\mathbb{R}$.

EReal.preimage_coe_Iic theorem

(y : ℝ) : Real.toEReal ⁻¹' Iic y = Iic y

Full source

@[simp]
lemma preimage_coe_Iic (y : ℝ) : Real.toERealReal.toEReal ⁻¹' Iic y = Iic y := by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Iic (WithBot.some (WithTop.some y))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Iic, WithTop.preimage_coe_Iic]

Preimage of Extended Real Interval $(-\infty, y]$ Equals Real Interval $(-\infty, y]$

Informal description

For any real number $y$, the preimage of the extended real interval $(-\infty, y]$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the real interval $(-\infty, y]$. In other words, $\text{Real.toEReal}^{-1}((-\infty, y]) = (-\infty, y]$.

EReal.preimage_coe_Iio theorem

(y : ℝ) : Real.toEReal ⁻¹' Iio y = Iio y

Full source

@[simp]
lemma preimage_coe_Iio (y : ℝ) : Real.toERealReal.toEReal ⁻¹' Iio y = Iio y := by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some (WithTop.some y))) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio]

Preimage of Extended Real Interval $(-\infty, y)$ Equals Real Interval $(-\infty, y)$

Informal description

For any real number $y$, the preimage of the extended real interval $(-\infty, y)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the real interval $(-\infty, y)$. In other words, $\text{Real.toEReal}^{-1}((-\infty, y)) = (-\infty, y)$.

EReal.preimage_coe_Iio_top theorem

: Real.toEReal ⁻¹' Iio ⊤ = univ

Full source

@[simp]
lemma preimage_coe_Iio_top : Real.toERealReal.toEReal ⁻¹' Iio ⊤ = univ := by
  change (WithBot.some ∘ WithTop.some) ⁻¹' (Iio (WithBot.some ⊤)) = _
  refine preimage_comp.trans ?_
  simp only [WithBot.preimage_coe_Iio, WithTop.preimage_coe_Iio_top]

Preimage of $(-\infty, \infty)$ under real inclusion is $\mathbb{R}$

Informal description

The preimage of the extended real interval $(-\infty, \top)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is the entire set of real numbers $\mathbb{R}$. In other words, $\text{Real.toEReal}^{-1}((-\infty, \top)) = \mathbb{R}$.

EReal.preimage_coe_Icc theorem

(x y : ℝ) : Real.toEReal ⁻¹' Icc x y = Icc x y

Full source

@[simp]
lemma preimage_coe_Icc (x y : ℝ) : Real.toERealReal.toEReal ⁻¹' Icc x y = Icc x y := by
  simp_rw [← Ici_inter_Iic]
  simp

Preimage of Extended Closed Interval Equals Real Closed Interval

Informal description

For any real numbers $x$ and $y$, the preimage of the extended closed interval $[x, y]$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the real closed interval $[x, y]$. In other words, $\text{Real.toEReal}^{-1}([x, y]) = [x, y]$.

EReal.preimage_coe_Ico theorem

(x y : ℝ) : Real.toEReal ⁻¹' Ico x y = Ico x y

Full source

@[simp]
lemma preimage_coe_Ico (x y : ℝ) : Real.toERealReal.toEReal ⁻¹' Ico x y = Ico x y := by
  simp_rw [← Ici_inter_Iio]
  simp

Preimage of Extended Interval $[x, y)$ Equals Real Interval $[x, y)$

Informal description

For any real numbers $x$ and $y$, the preimage of the extended interval $[x, y)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the real interval $[x, y)$. In other words, $\text{Real.toEReal}^{-1}([x, y)) = [x, y)$.

EReal.preimage_coe_Ioc theorem

(x y : ℝ) : Real.toEReal ⁻¹' Ioc x y = Ioc x y

Full source

@[simp]
lemma preimage_coe_Ioc (x y : ℝ) : Real.toERealReal.toEReal ⁻¹' Ioc x y = Ioc x y := by
  simp_rw [← Ioi_inter_Iic]
  simp

Preimage of Extended Interval $(x, y]$ Equals Real Interval $(x, y]$

Informal description

For any real numbers $x$ and $y$, the preimage of the extended real interval $(x, y]$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the real interval $(x, y]$. In other words, $\text{Real.toEReal}^{-1}((x, y]) = (x, y]$.

EReal.preimage_coe_Ioo theorem

(x y : ℝ) : Real.toEReal ⁻¹' Ioo x y = Ioo x y

Full source

@[simp]
lemma preimage_coe_Ioo (x y : ℝ) : Real.toERealReal.toEReal ⁻¹' Ioo x y = Ioo x y := by
  simp_rw [← Ioi_inter_Iio]
  simp

Preimage of Extended Open Interval Equals Real Open Interval

Informal description

For any real numbers $x$ and $y$, the preimage of the open interval $(x, y)$ in the extended real numbers $\overline{\mathbb{R}}$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the open interval $(x, y)$ in $\mathbb{R}$. In other words, $\text{Real.toEReal}^{-1}((x, y)) = (x, y)$.

EReal.preimage_coe_Ico_top theorem

(x : ℝ) : Real.toEReal ⁻¹' Ico x ⊤ = Ici x

Full source

@[simp]
lemma preimage_coe_Ico_top (x : ℝ) : Real.toERealReal.toEReal ⁻¹' Ico x ⊤ = Ici x := by
  rw [← Ici_inter_Iio]
  simp

Preimage of extended $[x, \infty)$ equals real $[x, \infty)$

Informal description

For any real number $x$, the preimage of the extended interval $[x, \infty)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the real interval $[x, \infty)$. In other words: $$\text{Real.toEReal}^{-1}([x, \infty)) = [x, \infty)$$

EReal.preimage_coe_Ioo_top theorem

(x : ℝ) : Real.toEReal ⁻¹' Ioo x ⊤ = Ioi x

Full source

@[simp]
lemma preimage_coe_Ioo_top (x : ℝ) : Real.toERealReal.toEReal ⁻¹' Ioo x ⊤ = Ioi x := by
  rw [← Ioi_inter_Iio]
  simp

Preimage of Extended Open Interval $(x, \infty)$ Equals Real Open Interval $(x, \infty)$

Informal description

For any real number $x$, the preimage of the extended open interval $(x, \infty)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the open interval $(x, \infty)$ in $\mathbb{R}$. That is, $\text{Real.toEReal}^{-1}((x, \infty)) = (x, \infty)$.

EReal.preimage_coe_Ioc_bot theorem

(y : ℝ) : Real.toEReal ⁻¹' Ioc ⊥ y = Iic y

Full source

@[simp]
lemma preimage_coe_Ioc_bot (y : ℝ) : Real.toERealReal.toEReal ⁻¹' Ioc ⊥ y = Iic y := by
  rw [← Ioi_inter_Iic]
  simp

Preimage of Extended $(\bot, y]$ Equals Real $(-\infty, y]$

Informal description

For any real number $y$, the preimage of the extended left-open right-closed interval $(-\infty, y]$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the real interval $(-\infty, y]$. In other words: $$\text{Real.toEReal}^{-1}((-\infty, y]) = (-\infty, y]$$

EReal.preimage_coe_Ioo_bot theorem

(y : ℝ) : Real.toEReal ⁻¹' Ioo ⊥ y = Iio y

Full source

@[simp]
lemma preimage_coe_Ioo_bot (y : ℝ) : Real.toERealReal.toEReal ⁻¹' Ioo ⊥ y = Iio y := by
  rw [← Ioi_inter_Iio]
  simp

Preimage of Extended Open Interval $(-\infty, y)$ Equals Real Open Interval $(-\infty, y)$

Informal description

For any real number $y$, the preimage of the extended open interval $(-\infty, y)$ under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is equal to the real open interval $(-\infty, y)$. That is, $\text{Real.toEReal}^{-1}((-\infty, y)) = (-\infty, y)$.

EReal.preimage_coe_Ioo_bot_top theorem

: Real.toEReal ⁻¹' Ioo ⊥ ⊤ = univ

Full source

@[simp]
lemma preimage_coe_Ioo_bot_top : Real.toERealReal.toEReal ⁻¹' Ioo ⊥ ⊤ = univ := by
  rw [← Ioi_inter_Iio]
  simp

Preimage of Extended Real Open Interval Under Inclusion is Entire Real Line

Informal description

The preimage of the open interval $(-\infty, \infty)$ in the extended real numbers under the canonical inclusion map $\mathbb{R} \to \overline{\mathbb{R}}$ is the entire set of real numbers $\mathbb{R}$. That is, $\text{Real.toEReal}^{-1}((-\infty, \infty)) = \mathbb{R}$.

EReal.toReal_coe_ennreal theorem

: ∀ {x : ℝ≥0∞}, toReal (x : EReal) = ENNReal.toReal x

Full source

@[simp]
theorem toReal_coe_ennreal : ∀ {x : ℝ≥0∞}, toReal (x : EReal) = ENNReal.toReal x
  | ⊤ => rfl
  | .some _ => rfl

Equality of Real Conversions for Extended Nonnegative Reals: $\text{toReal}(x) = \text{ENNReal.toReal}(x)$

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the real part of $x$ when viewed as an extended real number equals the standard conversion of $x$ to a real number, i.e., $\text{toReal}(x) = \text{ENNReal.toReal}(x)$.

EReal.coe_ennreal_ofReal theorem

{x : ℝ} : (ENNReal.ofReal x : EReal) = max x 0

Full source

@[simp]
theorem coe_ennreal_ofReal {x : ℝ} : (ENNReal.ofReal x : EReal) = max x 0 :=
  rfl

Inclusion of Extended Nonnegative Real from Real Preserves Maximum with Zero

Informal description

For any real number $x$, the extended real number obtained by first mapping $x$ to the extended nonnegative reals via $\text{ENNReal.ofReal}$ and then including it into the extended reals equals the maximum of $x$ and $0$, i.e., $(\text{ENNReal.ofReal}\, x : \overline{\mathbb{R}}) = \max(x, 0)$.

EReal.coe_ennreal_toReal theorem

{x : ℝ≥0∞} (hx : x ≠ ∞) : (x.toReal : EReal) = x

Full source

lemma coe_ennreal_toReal {x : ℝ≥0∞} (hx : x ≠ ∞) : (x.toReal : EReal) = x := by
  lift x to ℝ≥0 using hx
  rfl

Real Part Inclusion Preserves Finite Extended Nonnegative Reals

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $x \neq \infty$, the canonical inclusion of its real part into the extended reals equals $x$ itself, i.e., $x.\text{toReal} = x$ in $\overline{\mathbb{R}}$.

EReal.coe_nnreal_eq_coe_real theorem

(x : ℝ≥0) : ((x : ℝ≥0∞) : EReal) = (x : ℝ)

Full source

theorem coe_nnreal_eq_coe_real (x : ℝ≥0) : ((x : ℝ≥0∞) : EReal) = (x : ℝ) :=
  rfl

Equality of Extended Real Inclusions for Nonnegative Reals

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the inclusion of $x$ into the extended real numbers via the extended nonnegative reals equals the direct inclusion of $x$ into the extended reals, i.e., $x = x$ in $\overline{\mathbb{R}}$.

EReal.coe_ennreal_zero theorem

: ((0 : ℝ≥0∞) : EReal) = 0

Full source

@[simp, norm_cast]
theorem coe_ennreal_zero : ((0 : ℝ≥0∞) : EReal) = 0 :=
  rfl

Preservation of Additive Identity under Inclusion from Extended Nonnegative Reals to Extended Reals

Informal description

The inclusion map from extended nonnegative real numbers to extended real numbers maps the additive identity $0 \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ to the additive identity $0 \in \mathbb{R} \cup \{-\infty, \infty\}$, i.e., $((0 : \mathbb{R}_{\geq 0} \cup \{\infty\}) : \mathbb{R} \cup \{-\infty, \infty\}) = 0$.

EReal.coe_ennreal_one theorem

: ((1 : ℝ≥0∞) : EReal) = 1

Full source

@[simp, norm_cast]
theorem coe_ennreal_one : ((1 : ℝ≥0∞) : EReal) = 1 :=
  rfl

Preservation of Multiplicative Identity under Inclusion from Extended Nonnegative Reals to Extended Reals

Informal description

The inclusion map from extended nonnegative real numbers to extended real numbers maps the multiplicative identity $1 \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ to the multiplicative identity $1 \in \mathbb{R} \cup \{-\infty, \infty\}$, i.e., $((1 : \mathbb{R}_{\geq 0} \cup \{\infty\}) : \mathbb{R} \cup \{-\infty, \infty\}) = 1$.

EReal.coe_ennreal_top theorem

: ((⊤ : ℝ≥0∞) : EReal) = ⊤

Full source

@[simp, norm_cast]
theorem coe_ennreal_top : ((⊤ : ℝ≥0∞) : EReal) = ⊤ :=
  rfl

Preservation of Top Element under Inclusion from Extended Nonnegative Reals to Extended Reals

Informal description

The inclusion map from extended nonnegative real numbers to extended real numbers maps the top element $\top \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ to the top element $\top \in \mathbb{R} \cup \{-\infty, \infty\}$, i.e., $(\top : \mathbb{R}_{\geq 0} \cup \{\infty\}) = \top$ in $\overline{\mathbb{R}}$.

EReal.coe_ennreal_strictMono theorem

: StrictMono ((↑) : ℝ≥0∞ → EReal)

Full source

theorem coe_ennreal_strictMono : StrictMono ((↑) : ℝ≥0∞ → EReal) :=
  WithTop.strictMono_iff.2 ⟨fun _ _ => EReal.coe_lt_coe_iff.2, fun _ => coe_lt_top _⟩

Strict Monotonicity of Extended Nonnegative Real Inclusion into Extended Reals

Informal description

The inclusion map from extended nonnegative real numbers to extended real numbers is strictly monotone. That is, for any $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $x < y$, then $(x : \overline{\mathbb{R}}) < (y : \overline{\mathbb{R}})$.

EReal.coe_ennreal_injective theorem

: Injective ((↑) : ℝ≥0∞ → EReal)

Full source

theorem coe_ennreal_injective : Injective ((↑) : ℝ≥0∞ → EReal) :=
  coe_ennreal_strictMono.injective

Injectivity of the Extended Nonnegative Real Inclusion into Extended Reals

Informal description

The canonical inclusion map from extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ to extended real numbers $\mathbb{R} \cup \{-\infty, \infty\}$ is injective. That is, for any $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $(x : \overline{\mathbb{R}}) = (y : \overline{\mathbb{R}})$, then $x = y$.

EReal.coe_ennreal_eq_top_iff theorem

{x : ℝ≥0∞} : (x : EReal) = ⊤ ↔ x = ⊤

Full source

@[simp]
theorem coe_ennreal_eq_top_iff {x : ℝ≥0∞} : (x : EReal) = ⊤ ↔ x = ⊤ :=
  coe_ennreal_injective.eq_iff' rfl

Characterization of Extended Nonnegative Reals Mapping to Infinity in Extended Reals

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inclusion of $x$ into the extended real numbers $\overline{\mathbb{R}}$ equals the top element $\infty$ if and only if $x$ itself is $\infty$. In other words, $(x : \overline{\mathbb{R}}) = \infty \leftrightarrow x = \infty$.

EReal.coe_nnreal_ne_top theorem

(x : ℝ≥0) : ((x : ℝ≥0∞) : EReal) ≠ ⊤

Full source

theorem coe_nnreal_ne_top (x : ℝ≥0) : ((x : ℝ≥0∞) : EReal) ≠ ⊤ := coe_ne_top x

Nonnegative reals are not infinity in extended reals

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the extended real number obtained by first casting $x$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ and then to $\overline{\mathbb{R}}$ is not equal to the top element $\infty$, i.e., $x \neq \infty$ in $\overline{\mathbb{R}}$.

EReal.coe_nnreal_lt_top theorem

(x : ℝ≥0) : ((x : ℝ≥0∞) : EReal) < ⊤

Full source

@[simp]
theorem coe_nnreal_lt_top (x : ℝ≥0) : ((x : ℝ≥0∞) : EReal) < ⊤ := coe_lt_top x

Nonnegative reals are strictly below infinity in extended reals

Informal description

For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the extended real number obtained by first casting $x$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ and then to $\overline{\mathbb{R}}$ is strictly less than the top element $\infty$, i.e., $x < \infty$ in $\overline{\mathbb{R}}$.

EReal.coe_ennreal_le_coe_ennreal_iff theorem

{x y : ℝ≥0∞} : (x : EReal) ≤ (y : EReal) ↔ x ≤ y

Full source

@[simp, norm_cast]
theorem coe_ennreal_le_coe_ennreal_iff {x y : ℝ≥0∞} : (x : EReal) ≤ (y : EReal) ↔ x ≤ y :=
  coe_ennreal_strictMono.le_iff_le

Order Preservation of Extended Nonnegative Real Inclusion: $(x : \overline{\mathbb{R}}) \leq (y : \overline{\mathbb{R}}) \leftrightarrow x \leq y$

Informal description

For any extended nonnegative real numbers $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $(x : \overline{\mathbb{R}}) \leq (y : \overline{\mathbb{R}})$ holds if and only if $x \leq y$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

EReal.coe_ennreal_lt_coe_ennreal_iff theorem

{x y : ℝ≥0∞} : (x : EReal) < (y : EReal) ↔ x < y

Full source

@[simp, norm_cast]
theorem coe_ennreal_lt_coe_ennreal_iff {x y : ℝ≥0∞} : (x : EReal) < (y : EReal) ↔ x < y :=
  coe_ennreal_strictMono.lt_iff_lt

Preservation of Strict Inequality under Inclusion from Extended Nonnegative Reals to Extended Reals

Informal description

For any extended nonnegative real numbers $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $(x : \overline{\mathbb{R}}) < (y : \overline{\mathbb{R}})$ holds if and only if $x < y$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

EReal.coe_ennreal_eq_coe_ennreal_iff theorem

{x y : ℝ≥0∞} : (x : EReal) = (y : EReal) ↔ x = y

Full source

@[simp, norm_cast]
theorem coe_ennreal_eq_coe_ennreal_iff {x y : ℝ≥0∞} : (x : EReal) = (y : EReal) ↔ x = y :=
  coe_ennreal_injective.eq_iff

Equality Preservation of Extended Nonnegative Real Inclusion: $(x : \overline{\mathbb{R}}) = (y : \overline{\mathbb{R}}) \leftrightarrow x = y$

Informal description

For any extended nonnegative real numbers $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the equality $(x : \overline{\mathbb{R}}) = (y : \overline{\mathbb{R}})$ holds if and only if $x = y$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

EReal.coe_ennreal_ne_coe_ennreal_iff theorem

{x y : ℝ≥0∞} : (x : EReal) ≠ (y : EReal) ↔ x ≠ y

Full source

theorem coe_ennreal_ne_coe_ennreal_iff {x y : ℝ≥0∞} : (x : EReal) ≠ (y : EReal)(x : EReal) ≠ (y : EReal) ↔ x ≠ y :=
  coe_ennreal_injective.ne_iff

Inequality Preservation under Inclusion from Extended Nonnegative Reals to Extended Reals

Informal description

For any extended nonnegative real numbers $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $(x : \overline{\mathbb{R}}) \neq (y : \overline{\mathbb{R}})$ holds if and only if $x \neq y$.

EReal.coe_ennreal_eq_zero theorem

{x : ℝ≥0∞} : (x : EReal) = 0 ↔ x = 0

Full source

@[simp, norm_cast]
theorem coe_ennreal_eq_zero {x : ℝ≥0∞} : (x : EReal) = 0 ↔ x = 0 := by
  rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_zero]

Inclusion of Extended Nonnegative Reals Preserves Zero: $(x : \overline{\mathbb{R}}) = 0 \leftrightarrow x = 0$

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inclusion of $x$ into the extended real numbers equals $0$ if and only if $x = 0$. In other words, $(x : \overline{\mathbb{R}}) = 0 \leftrightarrow x = 0$.

EReal.coe_ennreal_eq_one theorem

{x : ℝ≥0∞} : (x : EReal) = 1 ↔ x = 1

Full source

@[simp, norm_cast]
theorem coe_ennreal_eq_one {x : ℝ≥0∞} : (x : EReal) = 1 ↔ x = 1 := by
  rw [← coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_one]

Equivalence of Extended Nonnegative Real Inclusion to One: $(x : \overline{\mathbb{R}}) = 1 \leftrightarrow x = 1$

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inclusion of $x$ into the extended real numbers equals $1$ if and only if $x = 1$, i.e., $(x : \overline{\mathbb{R}}) = 1 \leftrightarrow x = 1$.

EReal.coe_ennreal_ne_zero theorem

{x : ℝ≥0∞} : (x : EReal) ≠ 0 ↔ x ≠ 0

Full source

@[norm_cast]
theorem coe_ennreal_ne_zero {x : ℝ≥0∞} : (x : EReal) ≠ 0(x : EReal) ≠ 0 ↔ x ≠ 0 :=
  coe_ennreal_eq_zero.not

Nonzero Preservation in Extended Nonnegative Real Inclusion

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inclusion of $x$ into the extended real numbers is nonzero if and only if $x$ is nonzero, i.e., $(x : \overline{\mathbb{R}}) \neq 0 \leftrightarrow x \neq 0$.

EReal.coe_ennreal_ne_one theorem

{x : ℝ≥0∞} : (x : EReal) ≠ 1 ↔ x ≠ 1

Full source

@[norm_cast]
theorem coe_ennreal_ne_one {x : ℝ≥0∞} : (x : EReal) ≠ 1(x : EReal) ≠ 1 ↔ x ≠ 1 :=
  coe_ennreal_eq_one.not

Non-Equivalence of Extended Nonnegative Real Inclusion to One: $(x : \overline{\mathbb{R}}) \neq 1 \leftrightarrow x \neq 1$

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inclusion of $x$ into the extended real numbers is not equal to $1$ if and only if $x \neq 1$, i.e., $(x : \overline{\mathbb{R}}) \neq 1 \leftrightarrow x \neq 1$.

EReal.coe_ennreal_nonneg theorem

(x : ℝ≥0∞) : (0 : EReal) ≤ x

Full source

theorem coe_ennreal_nonneg (x : ℝ≥0∞) : (0 : EReal) ≤ x :=
  coe_ennreal_le_coe_ennreal_iff.2 (zero_le x)

Nonnegativity of Extended Nonnegative Reals in $\overline{\mathbb{R}}$

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $0 \leq x$ holds in the extended real numbers $\overline{\mathbb{R}}$.

EReal.range_coe_ennreal theorem

: range ((↑) : ℝ≥0∞ → EReal) = Set.Ici 0

Full source

@[simp] theorem range_coe_ennreal : range ((↑) : ℝ≥0∞ → EReal) = Set.Ici 0 :=
  Subset.antisymm (range_subset_iff.2 coe_ennreal_nonneg) fun x => match x with
    | ⊥ => fun h => absurd h bot_lt_zero.not_le
    | ⊤ => fun _ => ⟨⊤, rfl⟩
    | (x : ℝ) => fun h => ⟨.some ⟨x, EReal.coe_nonneg.1 h⟩, rfl⟩

Range of Extended Nonnegative Reals in $\overline{\mathbb{R}}$ is $[0, \infty)$

Informal description

The range of the canonical inclusion map from the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ to the extended real numbers $\overline{\mathbb{R}}$ is equal to the interval $[0, \infty)$ in $\overline{\mathbb{R}}$. In other words, $\text{range}(x \mapsto x) = [0, \infty)$.

EReal.instCanLiftENNRealToERealLeOfNat instance

: CanLift EReal ℝ≥0∞ (↑) (0 ≤ ·)

Full source

instance : CanLift EReal ℝ≥0∞ (↑) (0 ≤ ·) := ⟨range_coe_ennreal.ge⟩

Lifting Condition from Extended Reals to Extended Nonnegative Reals

Informal description

The extended real numbers $\overline{\mathbb{R}}$ can be lifted to the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ via the canonical inclusion map, with the condition that the element is nonnegative (i.e., $0 \leq \cdot$).

EReal.coe_ennreal_pos theorem

{x : ℝ≥0∞} : (0 : EReal) < x ↔ 0 < x

Full source

@[simp, norm_cast]
theorem coe_ennreal_pos {x : ℝ≥0∞} : (0 : EReal) < x ↔ 0 < x := by
  rw [← coe_ennreal_zero, coe_ennreal_lt_coe_ennreal_iff]

Positivity Preservation for Extended Nonnegative Reals in Extended Reals

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $0 < x$ holds in the extended real numbers $\overline{\mathbb{R}}$ if and only if $0 < x$ holds in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

EReal.bot_lt_coe_ennreal theorem

(x : ℝ≥0∞) : (⊥ : EReal) < x

Full source

@[simp]
theorem bot_lt_coe_ennreal (x : ℝ≥0∞) : (⊥ : EReal) < x :=
  (bot_lt_coe 0).trans_le (coe_ennreal_nonneg _)

$-\infty$ is less than any extended nonnegative real number

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the bottom element $-\infty$ of the extended real numbers is strictly less than $x$, i.e., $-\infty < x$.

EReal.coe_ennreal_ne_bot theorem

(x : ℝ≥0∞) : (x : EReal) ≠ ⊥

Full source

@[simp]
theorem coe_ennreal_ne_bot (x : ℝ≥0∞) : (x : EReal) ≠ ⊥ :=
  (bot_lt_coe_ennreal x).ne'

Nonnegative Extended Reals Exclude Negative Infinity

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inclusion of $x$ into the extended real numbers $\overline{\mathbb{R}}$ is not equal to the bottom element $-\infty$, i.e., $x \neq -\infty$.

EReal.coe_ennreal_add theorem

(x y : ENNReal) : ((x + y : ℝ≥0∞) : EReal) = x + y

Full source

@[simp, norm_cast]
theorem coe_ennreal_add (x y : ENNReal) : ((x + y : ℝ≥0∞) : EReal) = x + y := by
  cases x <;> cases y <;> rfl

Additivity of Inclusion from Extended Nonnegative Reals to Extended Reals

Informal description

For any extended nonnegative real numbers $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inclusion map satisfies $(x + y) = x + y$ in the extended real numbers $\overline{\mathbb{R}}$.

EReal.coe_ennreal_mul theorem

: ∀ x y : ℝ≥0∞, ((x * y : ℝ≥0∞) : EReal) = (x : EReal) * y

Full source

@[simp, norm_cast]
theorem coe_ennreal_mul : ∀ x y : ℝ≥0∞, ((x * y : ℝ≥0∞) : EReal) = (x : EReal) * y
  | ⊤, ⊤ => rfl
  | ⊤, (y : ℝ≥0) => coe_ennreal_top_mul y
  | (x : ℝ≥0), ⊤ => by
    rw [mul_comm, coe_ennreal_top_mul, EReal.mul_comm, coe_ennreal_top]
  | (x : ℝ≥0), (y : ℝ≥0) => by
    simp only [← ENNReal.coe_mul, coe_nnreal_eq_coe_real, NNReal.coe_mul, EReal.coe_mul]

Multiplication Preservation under Inclusion from Extended Nonnegative Reals to Extended Reals

Informal description

For any extended nonnegative real numbers $x, y \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inclusion map from extended nonnegative reals to extended reals preserves multiplication, i.e., $(x \cdot y) = x \cdot y$ in $\overline{\mathbb{R}}$.

EReal.coe_ennreal_nsmul theorem

(n : ℕ) (x : ℝ≥0∞) : (↑(n • x) : EReal) = n • (x : EReal)

Full source

@[norm_cast]
theorem coe_ennreal_nsmul (n : ℕ) (x : ℝ≥0∞) : (↑(n • x) : EReal) = n • (x : EReal) :=
  map_nsmul (⟨⟨(↑), coe_ennreal_zero⟩, coe_ennreal_add⟩ : ℝ≥0∞ℝ≥0∞ →+ EReal) _ _

Preservation of Scalar Multiplication under Inclusion from Extended Nonnegative Reals to Extended Reals

Informal description

For any natural number $n$ and any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inclusion map from extended nonnegative reals to extended reals preserves scalar multiplication, i.e., $(n \cdot x) = n \cdot x$ in $\overline{\mathbb{R}}$.

EReal.toENNReal definition

(x : EReal) : ℝ≥0∞

Full source

/-- `x.toENNReal` returns `x` if it is nonnegative, `0` otherwise. -/
noncomputable def toENNReal (x : EReal) : ℝ≥0∞ :=
  if x = ⊤ then ⊤
  else ENNReal.ofReal x.toReal

Conversion from extended real to extended non-negative real numbers

Informal description

The function maps an extended real number $ x \in \overline{\mathbb{R}} $ to an extended non-negative real number as follows: if $ x $ is $ \top $ (positive infinity), it returns $ \top $; otherwise, it returns the non-negative real number obtained by converting $ x $ to a real number (treating $ -\infty $ as $ 0 $) and then to an extended non-negative real number.

EReal.toENNReal_top theorem

: (⊤ : EReal).toENNReal = ⊤

Full source

@[simp] lemma toENNReal_top : (⊤ : EReal).toENNReal = ⊤ := rfl

Conversion of Top Element in Extended Real Numbers to Extended Non-Negative Real Numbers

Informal description

The conversion of the top element $\top$ in the extended real numbers to an extended non-negative real number is equal to the top element $\top$ in the extended non-negative real numbers, i.e., $\text{toENNReal}(\top) = \top$.

EReal.toENNReal_of_ne_top theorem

{x : EReal} (hx : x ≠ ⊤) : x.toENNReal = ENNReal.ofReal x.toReal

Full source

@[simp]
lemma toENNReal_of_ne_top {x : EReal} (hx : x ≠ ⊤) : x.toENNReal = ENNReal.ofReal x.toReal :=
  if_neg hx

Conversion of Non-Infinite Extended Real to Extended Non-Negative Real

Informal description

For any extended real number $x \neq \infty$, the conversion of $x$ to an extended non-negative real number equals the extended non-negative real number obtained from the real part of $x$, i.e., $\text{toENNReal}(x) = \text{ENNReal.ofReal}(\text{toReal}(x))$.

EReal.toENNReal_eq_top_iff theorem

{x : EReal} : x.toENNReal = ⊤ ↔ x = ⊤

Full source

@[simp]
lemma toENNReal_eq_top_iff {x : EReal} : x.toENNReal = ⊤ ↔ x = ⊤ := by
  by_cases h : x = ⊤
  · simp [h]
  · simp [h, toENNReal]

Characterization of Extended Real to Extended Non-Negative Real Conversion at Infinity: $x.\text{toENNReal} = \infty \leftrightarrow x = \infty$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the conversion of $x$ to an extended non-negative real number equals $\infty$ if and only if $x$ itself is $\infty$. In other words, $x.\text{toENNReal} = \infty \leftrightarrow x = \infty$.

EReal.toENNReal_ne_top_iff theorem

{x : EReal} : x.toENNReal ≠ ⊤ ↔ x ≠ ⊤

Full source

lemma toENNReal_ne_top_iff {x : EReal} : x.toENNReal ≠ ⊤x.toENNReal ≠ ⊤ ↔ x ≠ ⊤ := toENNReal_eq_top_iff.not

Non-Infinity Characterization for Extended Real to Extended Non-Negative Real Conversion

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the conversion of $x$ to an extended non-negative real number is not equal to $\infty$ if and only if $x$ itself is not equal to $\infty$. In other words, $x.\text{toENNReal} \neq \infty \leftrightarrow x \neq \infty$.

EReal.toENNReal_of_nonpos theorem

{x : EReal} (hx : x ≤ 0) : x.toENNReal = 0

Full source

@[simp]
lemma toENNReal_of_nonpos {x : EReal} (hx : x ≤ 0) : x.toENNReal = 0 := by
  rw [toENNReal, if_neg (fun h ↦ ?_)]
  · exact ENNReal.ofReal_of_nonpos (toReal_nonpos hx)
  · exact zero_ne_top <| top_le_iff.mp <| h ▸ hx

Conversion of Non-Positive Extended Real to Zero in Extended Non-Negative Reals

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$ such that $x \leq 0$, the conversion of $x$ to an extended non-negative real number equals $0$, i.e., $x.\text{toENNReal} = 0$.

EReal.toENNReal_bot theorem

: (⊥ : EReal).toENNReal = 0

Full source

lemma toENNReal_bot : (⊥ : EReal).toENNReal = 0 := toENNReal_of_nonpos bot_le

Conversion of $-\infty$ to Zero in Extended Non-Negative Reals

Informal description

The conversion of the bottom element $-\infty$ in the extended real numbers to an extended non-negative real number equals $0$, i.e., $(-\infty).\text{toENNReal} = 0$.

EReal.toENNReal_zero theorem

: (0 : EReal).toENNReal = 0

Full source

lemma toENNReal_zero : (0 : EReal).toENNReal = 0 := toENNReal_of_nonpos le_rfl

Conversion of Zero in Extended Reals to Zero in Extended Non-Negative Reals

Informal description

The conversion of the extended real number $0$ to an extended non-negative real number equals $0$, i.e., $0.\text{toENNReal} = 0$.

EReal.toENNReal_eq_zero_iff theorem

{x : EReal} : x.toENNReal = 0 ↔ x ≤ 0

Full source

lemma toENNReal_eq_zero_iff {x : EReal} : x.toENNReal = 0 ↔ x ≤ 0 := by
  induction x <;> simp [toENNReal]

Characterization of Zero in Extended Non-Negative Reals: $x_{\text{ENN}} = 0 \leftrightarrow x \leq 0$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the conversion of $x$ to an extended non-negative real number equals $0$ if and only if $x \leq 0$.

EReal.toENNReal_ne_zero_iff theorem

{x : EReal} : x.toENNReal ≠ 0 ↔ 0 < x

Full source

lemma toENNReal_ne_zero_iff {x : EReal} : x.toENNReal ≠ 0x.toENNReal ≠ 0 ↔ 0 < x := by
  simp [toENNReal_eq_zero_iff.not]

Nonzero Characterization of Extended Non-Negative Reals: $x_{\text{ENN}} \neq 0 \leftrightarrow 0 < x$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the conversion of $x$ to an extended non-negative real number is nonzero if and only if $x$ is strictly greater than zero, i.e., $x_{\text{ENN}} \neq 0 \leftrightarrow 0 < x$.

EReal.coe_toENNReal theorem

{x : EReal} (hx : 0 ≤ x) : (x.toENNReal : EReal) = x

Full source

@[simp]
lemma coe_toENNReal {x : EReal} (hx : 0 ≤ x) : (x.toENNReal : EReal) = x := by
  rw [toENNReal]
  by_cases h_top : x = ⊤
  · rw [if_pos h_top, h_top]
    rfl
  rw [if_neg h_top]
  simp only [coe_ennreal_ofReal, ge_iff_le, hx, toReal_nonneg, max_eq_left]
  exact coe_toReal h_top fun _ ↦ by simp_all only [le_bot_iff, zero_ne_bot]

Canonical Inclusion Preserves Nonnegative Extended Reals under `toENNReal` Conversion

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$ such that $0 \leq x$, the canonical inclusion of the extended nonnegative real number obtained by applying the `toENNReal` function to $x$ equals $x$ itself, i.e., $\overline{x.\text{toENNReal}} = x$.

EReal.coe_toENNReal_eq_max theorem

{x : EReal} : x.toENNReal = max 0 x

Full source

lemma coe_toENNReal_eq_max {x : EReal} : x.toENNReal = max 0 x := by
  rcases le_total 0 x with (hx | hx)
  · rw [coe_toENNReal hx, max_eq_right hx]
  · rw [toENNReal_of_nonpos hx, max_eq_left hx, coe_ennreal_zero]

Conversion to Extended Non-Negative Reals as Maximum: $x_{\text{ENN}} = \max(0, x)$

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$, the conversion of $x$ to an extended non-negative real number via `toENNReal` equals the maximum of $0$ and $x$, i.e., $x.\text{toENNReal} = \max(0, x)$.

EReal.toENNReal_coe theorem

{x : ℝ≥0∞} : (x : EReal).toENNReal = x

Full source

@[simp]
lemma toENNReal_coe {x : ℝ≥0∞} : (x : EReal).toENNReal = x := by
  by_cases h_top : x = ⊤
  · rw [h_top, coe_ennreal_top, toENNReal_top]
  rwa [toENNReal, if_neg _, toReal_coe_ennreal, ENNReal.ofReal_toReal_eq_iff]
  simp [h_top]

Preservation of Extended Nonnegative Reals under Conversion: $(x : \overline{\mathbb{R}}).\text{toENNReal} = x$

Informal description

For any extended nonnegative real number $x \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the conversion of $x$ to an extended real number and then back to an extended nonnegative real number via `toENNReal` yields $x$ itself, i.e., $(x : \overline{\mathbb{R}}).\text{toENNReal} = x$.

EReal.real_coe_toENNReal theorem

(x : ℝ) : (x : EReal).toENNReal = ENNReal.ofReal x

Full source

@[simp] lemma real_coe_toENNReal (x : ℝ) : (x : EReal).toENNReal = ENNReal.ofReal x := rfl

Compatibility of Real Coercion with Extended Non-Negative Real Conversion

Informal description

For any real number $x$, the extended non-negative real number obtained by first coercing $x$ to an extended real number and then applying the `toENNReal` function is equal to the extended non-negative real number obtained by applying the `ENNReal.ofReal` function directly to $x$. In other words, $(x : \overline{\mathbb{R}}).\text{toENNReal} = \text{ENNReal.ofReal}(x)$.

EReal.toReal_toENNReal theorem

{x : EReal} (hx : 0 ≤ x) : x.toENNReal.toReal = x.toReal

Full source

@[simp]
lemma toReal_toENNReal {x : EReal} (hx : 0 ≤ x) : x.toENNReal.toReal = x.toReal := by
  by_cases h : x = ⊤
  · simp [h]
  · simp [h, toReal_nonneg hx]

Compatibility of Real Conversion with Extended Non-Negative Real Conversion for Non-Negative Extended Reals

Informal description

For any extended real number $x \in \overline{\mathbb{R}}$ such that $0 \leq x$, the real part of the extended non-negative real number obtained by converting $x$ equals the real part of $x$ itself, i.e., $\text{toReal}(\text{toENNReal}(x)) = \text{toReal}(x)$.

EReal.toENNReal_eq_toENNReal theorem

{x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) : x.toENNReal = y.toENNReal ↔ x = y

Full source

lemma toENNReal_eq_toENNReal {x y : EReal} (hx : 0 ≤ x) (hy : 0 ≤ y) :
    x.toENNReal = y.toENNReal ↔ x = y := by
  induction x <;> induction y <;> simp_all

Equivalence of Equality for Non-Negative Extended Reals and Their Extended Non-Negative Real Conversions

Informal description

For any extended real numbers $x, y \in \overline{\mathbb{R}}$ such that $0 \leq x$ and $0 \leq y$, the equality of their conversions to extended non-negative real numbers is equivalent to the equality of $x$ and $y$ themselves. That is, $\text{toENNReal}(x) = \text{toENNReal}(y) \leftrightarrow x = y$.

EReal.toENNReal_le_toENNReal theorem

{x y : EReal} (h : x ≤ y) : x.toENNReal ≤ y.toENNReal

Full source

lemma toENNReal_le_toENNReal {x y : EReal} (h : x ≤ y) : x.toENNReal ≤ y.toENNReal := by
  induction x
  · simp
  · by_cases hy_top : y = ⊤
    · simp [hy_top]
    simp only [toENNReal, coe_ne_top, ↓reduceIte, toReal_coe, hy_top]
    exact ENNReal.ofReal_le_ofReal <| EReal.toReal_le_toReal h (coe_ne_bot _) hy_top
  · simp_all

Monotonicity of Extended Real to Extended Non-Negative Real Conversion: $x \leq y \Rightarrow \text{toENNReal}(x) \leq \text{toENNReal}(y)$

Informal description

For any extended real numbers $x$ and $y$ such that $x \leq y$, the inequality $\text{toENNReal}(x) \leq \text{toENNReal}(y)$ holds, where $\text{toENNReal}$ maps extended reals to extended non-negative reals by sending $\infty$ to $\infty$, finite values to their non-negative real counterparts (with $-\infty$ mapped to $0$).

EReal.toENNReal_lt_toENNReal theorem

{x y : EReal} (hx : 0 ≤ x) (hxy : x < y) : x.toENNReal < y.toENNReal

Full source

lemma toENNReal_lt_toENNReal {x y : EReal} (hx : 0 ≤ x) (hxy : x < y) :
    x.toENNReal < y.toENNReal :=
  lt_of_le_of_ne (toENNReal_le_toENNReal hxy.le)
    fun h ↦ hxy.ne <| (toENNReal_eq_toENNReal hx (hx.trans_lt hxy).le).mp h

Strict Monotonicity of Extended Real to Extended Non-Negative Real Conversion: $0 \leq x < y \Rightarrow \text{toENNReal}(x) < \text{toENNReal}(y)$

Informal description

For any extended real numbers $x, y \in \overline{\mathbb{R}}$ such that $0 \leq x$ and $x < y$, the strict inequality $\text{toENNReal}(x) < \text{toENNReal}(y)$ holds, where $\text{toENNReal}$ maps extended reals to extended non-negative reals by sending $\infty$ to $\infty$, finite values to their non-negative real counterparts (with $-\infty$ mapped to $0$).

EReal.coe_coe_eq_natCast theorem

(n : ℕ) : (n : ℝ) = (n : EReal)

Full source

theorem coe_coe_eq_natCast (n : ℕ) : (n : ℝ) = (n : EReal) := rfl

Natural Number Cast Commutes with Real and Extended Real Coercions

Informal description

For any natural number $n$, the extended real number obtained by casting $n$ to $\overline{\mathbb{R}}$ is equal to the extended real number obtained by first casting $n$ to $\mathbb{R}$ and then to $\overline{\mathbb{R}}$. In other words, $(n : \mathbb{R}) = (n : \overline{\mathbb{R}})$.

EReal.natCast_ne_bot theorem

(n : ℕ) : (n : EReal) ≠ ⊥

Full source

theorem natCast_ne_bot (n : ℕ) : (n : EReal) ≠ ⊥ := Ne.symm (ne_of_beq_false rfl)

Natural Number Cast in Extended Reals is Not Negative Infinity

Informal description

For any natural number $n$, the extended real number obtained by casting $n$ to $\overline{\mathbb{R}}$ is not equal to $-\infty$ (denoted as $\bot$).

EReal.natCast_ne_top theorem

(n : ℕ) : (n : EReal) ≠ ⊤

Full source

theorem natCast_ne_top (n : ℕ) : (n : EReal) ≠ ⊤ := Ne.symm (ne_of_beq_false rfl)

Natural Number Cast in Extended Reals is Not Infinity

Informal description

For any natural number $n$, the extended real number obtained by casting $n$ to $\overline{\mathbb{R}}$ is not equal to $\infty$ (denoted as $\top$).

EReal.natCast_eq_iff theorem

{m n : ℕ} : (m : EReal) = (n : EReal) ↔ m = n

Full source

@[norm_cast]
theorem natCast_eq_iff {m n : ℕ} : (m : EReal) = (n : EReal) ↔ m = n := by
  rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_eq_coe_iff, Nat.cast_inj]

Equality of Natural Number Casts in Extended Reals: $(m : \overline{\mathbb{R}}) = (n : \overline{\mathbb{R}}) \leftrightarrow m = n$

Informal description

For any natural numbers $m$ and $n$, the equality $(m : \overline{\mathbb{R}}) = (n : \overline{\mathbb{R}})$ holds in the extended real numbers if and only if $m = n$ in $\mathbb{N}$.

EReal.natCast_ne_iff theorem

{m n : ℕ} : (m : EReal) ≠ (n : EReal) ↔ m ≠ n

Full source

theorem natCast_ne_iff {m n : ℕ} : (m : EReal) ≠ (n : EReal)(m : EReal) ≠ (n : EReal) ↔ m ≠ n :=
  not_iff_not.2 natCast_eq_iff

Inequality Preservation under Natural Number Cast to Extended Reals: $(m : \overline{\mathbb{R}}) \neq (n : \overline{\mathbb{R}}) \leftrightarrow m \neq n$

Informal description

For any natural numbers $m$ and $n$, the inequality $(m : \overline{\mathbb{R}}) \neq (n : \overline{\mathbb{R}})$ holds in the extended real numbers if and only if $m \neq n$ holds in $\mathbb{N}$.

EReal.natCast_le_iff theorem

{m n : ℕ} : (m : EReal) ≤ (n : EReal) ↔ m ≤ n

Full source

@[norm_cast]
theorem natCast_le_iff {m n : ℕ} : (m : EReal) ≤ (n : EReal) ↔ m ≤ n := by
  rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_le_coe_iff, Nat.cast_le]

Preservation of Order under Natural Number Cast to Extended Reals: $(m : \overline{\mathbb{R}}) \leq (n : \overline{\mathbb{R}}) \leftrightarrow m \leq n$

Informal description

For any natural numbers $m$ and $n$, the inequality $(m : \overline{\mathbb{R}}) \leq (n : \overline{\mathbb{R}})$ holds in the extended real numbers if and only if $m \leq n$ holds in $\mathbb{N}$.

EReal.natCast_lt_iff theorem

{m n : ℕ} : (m : EReal) < (n : EReal) ↔ m < n

Full source

@[norm_cast]
theorem natCast_lt_iff {m n : ℕ} : (m : EReal) < (n : EReal) ↔ m < n := by
  rw [← coe_coe_eq_natCast n, ← coe_coe_eq_natCast m, EReal.coe_lt_coe_iff, Nat.cast_lt]

Preservation of Strict Order under Natural Number Cast to Extended Reals: $(m : \overline{\mathbb{R}}) < (n : \overline{\mathbb{R}}) \leftrightarrow m < n$

Informal description

For any natural numbers $m$ and $n$, the inequality $(m : \overline{\mathbb{R}}) < (n : \overline{\mathbb{R}})$ holds in the extended real numbers if and only if $m < n$ holds in the natural numbers.

EReal.natCast_mul theorem

(m n : ℕ) : (m * n : ℕ) = (m : EReal) * (n : EReal)

Full source

@[simp, norm_cast]
theorem natCast_mul (m n : ℕ) :
    (m * n : ℕ) = (m : EReal) * (n : EReal) := by
  rw [← coe_coe_eq_natCast, ← coe_coe_eq_natCast, ← coe_coe_eq_natCast, Nat.cast_mul, EReal.coe_mul]

Preservation of Multiplication under Natural Number Cast to Extended Reals: $(m \cdot n : \overline{\mathbb{R}}) = (m : \overline{\mathbb{R}}) \cdot (n : \overline{\mathbb{R}})$

Informal description

For any natural numbers $m$ and $n$, the extended real number obtained by casting the product $m \cdot n$ is equal to the product of the extended real numbers obtained by casting $m$ and $n$ individually, i.e., $(m \cdot n : \overline{\mathbb{R}}) = (m : \overline{\mathbb{R}}) \cdot (n : \overline{\mathbb{R}})$.

EReal.exists_rat_btwn_of_lt theorem

: ∀ {a b : EReal}, a < b → ∃ x : ℚ, a < (x : ℝ) ∧ ((x : ℝ) : EReal) < b

Full source

theorem exists_rat_btwn_of_lt :
    ∀ {a b : EReal}, a < b → ∃ x : ℚ, a < (x : ℝ) ∧ ((x : ℝ) : EReal) < b
  | ⊤, _, h => (not_top_lt h).elim
  | (a : ℝ), ⊥, h => (lt_irrefl _ ((bot_lt_coe a).trans h)).elim
  | (a : ℝ), (b : ℝ), h => by simp [exists_rat_btwn (EReal.coe_lt_coe_iff.1 h)]
  | (a : ℝ), ⊤, _ =>
    let ⟨b, hab⟩ := exists_rat_gt a
    ⟨b, by simpa using hab, coe_lt_top _⟩
  | ⊥, ⊥, h => (lt_irrefl _ h).elim
  | ⊥, (a : ℝ), _ =>
    let ⟨b, hab⟩ := exists_rat_lt a
    ⟨b, bot_lt_coe _, by simpa using hab⟩
  | ⊥, ⊤, _ => ⟨0, bot_lt_coe _, coe_lt_top _⟩

Existence of Rational Between Extended Reals

Informal description

For any extended real numbers $a$ and $b$ such that $a < b$, there exists a rational number $x$ such that $a < x$ as real numbers and the inclusion of $x$ in the extended reals satisfies $x < b$.

EReal.lt_iff_exists_rat_btwn theorem

{a b : EReal} : a < b ↔ ∃ x : ℚ, a < (x : ℝ) ∧ ((x : ℝ) : EReal) < b

Full source

theorem lt_iff_exists_rat_btwn {a b : EReal} :
    a < b ↔ ∃ x : ℚ, a < (x : ℝ) ∧ ((x : ℝ) : EReal) < b :=
  ⟨fun hab => exists_rat_btwn_of_lt hab, fun ⟨_x, ax, xb⟩ => ax.trans xb⟩

Characterization of Extended Real Inequality via Rational Intermediates: $a < b \leftrightarrow \exists x \in \mathbb{Q}, a < x < b$

Informal description

For any extended real numbers $a$ and $b$, the inequality $a < b$ holds if and only if there exists a rational number $x$ such that $a < x$ as real numbers and the inclusion of $x$ in the extended reals satisfies $x < b$.

EReal.lt_iff_exists_real_btwn theorem

{a b : EReal} : a < b ↔ ∃ x : ℝ, a < x ∧ (x : EReal) < b

Full source

theorem lt_iff_exists_real_btwn {a b : EReal} : a < b ↔ ∃ x : ℝ, a < x ∧ (x : EReal) < b :=
  ⟨fun hab =>
    let ⟨x, ax, xb⟩ := exists_rat_btwn_of_lt hab
    ⟨(x : ℝ), ax, xb⟩,
    fun ⟨_x, ax, xb⟩ => ax.trans xb⟩

Characterization of Extended Real Order via Intermediate Reals

Informal description

For any extended real numbers $a$ and $b$, the inequality $a < b$ holds if and only if there exists a real number $x$ such that $a < x$ and the inclusion of $x$ in the extended reals satisfies $x < b$.

EReal.neTopBotEquivReal definition

: ({⊥, ⊤}ᶜ : Set EReal) ≃ ℝ

Full source

/-- The set of numbers in `EReal` that are not equal to `±∞` is equivalent to `ℝ`. -/
def neTopBotEquivReal : ({⊥, ⊤}ᶜ : Set EReal) ≃ ℝ where
  toFun x := EReal.toReal x
  invFun x := ⟨x, by simp⟩
  left_inv := fun ⟨x, hx⟩ => by
    lift x to ℝ
    · simpa [not_or, and_comm] using hx
    · simp
  right_inv x := by simp

Bijection between finite extended reals and reals

Informal description

The set of extended real numbers $\overline{\mathbb{R}}$ excluding $\pm\infty$ (i.e., $\overline{\mathbb{R}} \setminus \{\top, \bot\}$) is in bijection with the real numbers $\mathbb{R}$. The bijection is given by the canonical projection from finite extended reals to reals, with its inverse being the inclusion of reals into extended reals.

Tags