doc-next-gen

Mathlib.Data.ENNReal.Operations

Module docstring

{"# Properties of addition, multiplication and subtraction on extended non-negative real numbers

In this file we prove elementary properties of algebraic operations on ℝ≥0∞, including addition, multiplication, natural powers and truncated subtraction, as well as how these interact with the order structure on ℝ≥0∞. Notably excluded from this list are inversion and division, the definitions and properties of which can be found in Mathlib.Data.ENNReal.Inv.

Note: the definitions of the operations included in this file can be found in Mathlib.Data.ENNReal.Basic. "}

ENNReal.mul_lt_mul theorem
(ac : a < c) (bd : b < d) : a * b < c * d
Full source 
@[mono, gcongr]
theorem mul_lt_mul (ac : a < c) (bd : b < d) : a * b < c * d := WithTop.mul_lt_mul ac bd
Strict Monotonicity of Multiplication in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b, c, d \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a < c$ and $b < d$, then $a \cdot b < c \cdot d$.
ENNReal.pow_right_strictMono theorem
{n : ℕ} (hn : n ≠ 0) : StrictMono fun a : ℝ≥0∞ ↦ a ^ n
Full source 
protected lemma pow_right_strictMono {n : ℕ} (hn : n ≠ 0) : StrictMono fun a : ℝ≥0∞ ↦ a ^ n :=
  WithTop.pow_right_strictMono hn
Strict Monotonicity of Power Function on Extended Non-Negative Reals for Nonzero Exponents
Informal description
For any natural number $n \neq 0$, the function $a \mapsto a^n$ is strictly monotone on the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$. That is, for any $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a < b$ then $a^n < b^n$.
ENNReal.pow_lt_pow_left theorem
(hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n
Full source 
@[gcongr] protected lemma pow_lt_pow_left (hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n :=
  WithTop.pow_lt_pow_left hab hn
Strict Monotonicity of Powers in Extended Non-Negative Reals for Nonzero Exponents
Informal description
For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a < b$, and for any natural number $n \neq 0$, we have $a^n < b^n$.
ENNReal.mul_left_strictMono theorem
(h0 : a ≠ 0) (hinf : a ≠ ∞) : StrictMono (a * ·)
Full source 
theorem mul_left_strictMono (h0 : a ≠ 0) (hinf : a ≠ ∞) : StrictMono (a * ·) := by
  lift a to ℝ≥0 using hinf
  rw [coe_ne_zero] at h0
  intro x y h
  contrapose! h
  simpa only [← mul_assoc, ← coe_mul, inv_mul_cancel₀ h0, coe_one, one_mul]
    using mul_le_mul_left' h (↑a⁻¹)
Strict Monotonicity of Left Multiplication in Extended Non-Negative Real Numbers
Informal description
For any extended non-negative real number $a$ such that $a \neq 0$ and $a \neq \infty$, the function $x \mapsto a \cdot x$ is strictly monotone. That is, for any $b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $b < c$ then $a \cdot b < a \cdot c$.
ENNReal.mul_lt_mul_left' theorem
(h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) : a * b < a * c
Full source 
@[gcongr] protected theorem mul_lt_mul_left' (h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) :
    a * b < a * c :=
  ENNReal.mul_left_strictMono h0 hinf bc
Strict Inequality Preservation under Left Multiplication in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$, $b$, and $c$ such that $a \neq 0$ and $a \neq \infty$, if $b < c$, then $a \cdot b < a \cdot c$.
ENNReal.mul_lt_mul_right' theorem
(h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) : b * a < c * a
Full source 
@[gcongr] protected theorem mul_lt_mul_right' (h0 : a ≠ 0) (hinf : a ≠ ⊤) (bc : b < c) :
    b * a < c * a :=
  mul_comm b a ▸ mul_comm c a ▸ ENNReal.mul_left_strictMono h0 hinf bc
Strict Monotonicity of Right Multiplication in Extended Non-Negative Real Numbers
Informal description
For any extended non-negative real number $a$ such that $a \neq 0$ and $a \neq \infty$, and for any $b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $b < c$, it holds that $b \cdot a < c \cdot a$.
ENNReal.mul_right_inj theorem
(h0 : a ≠ 0) (hinf : a ≠ ∞) : a * b = a * c ↔ b = c
Full source 
protected theorem mul_right_inj (h0 : a ≠ 0) (hinf : a ≠ ∞) : a * b = a * c ↔ b = c :=
  (mul_left_strictMono h0 hinf).injective.eq_iff
Right Cancellation Property for Multiplication in Extended Non-Negative Real Numbers
Informal description
For any extended non-negative real number $a$ such that $a \neq 0$ and $a \neq \infty$, the equality $a \cdot b = a \cdot c$ holds if and only if $b = c$.
ENNReal.mul_left_inj theorem
(h0 : c ≠ 0) (hinf : c ≠ ∞) : a * c = b * c ↔ a = b
Full source 
protected theorem mul_left_inj (h0 : c ≠ 0) (hinf : c ≠ ∞) : a * c = b * c ↔ a = b :=
  mul_comm c a ▸ mul_comm c b ▸ ENNReal.mul_right_inj h0 hinf
Left Cancellation Property for Multiplication in Extended Non-Negative Real Numbers
Informal description
For any extended non-negative real number $c$ such that $c \neq 0$ and $c \neq \infty$, the equality $a \cdot c = b \cdot c$ holds if and only if $a = b$.
ENNReal.mul_le_mul_left theorem
(h0 : a ≠ 0) (hinf : a ≠ ∞) : a * b ≤ a * c ↔ b ≤ c
Full source 
theorem mul_le_mul_left (h0 : a ≠ 0) (hinf : a ≠ ∞) : a * b ≤ a * c ↔ b ≤ c :=
  (mul_left_strictMono h0 hinf).le_iff_le
Left Multiplication Preserves Order in Extended Non-Negative Real Numbers
Informal description
For any extended non-negative real number $a$ such that $a \neq 0$ and $a \neq \infty$, and for any $b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a \cdot b \leq a \cdot c$ holds if and only if $b \leq c$.
ENNReal.mul_le_mul_right theorem
: c ≠ 0 → c ≠ ∞ → (a * c ≤ b * c ↔ a ≤ b)
Full source 
theorem mul_le_mul_right : c ≠ 0 → c ≠ ∞ → (a * c ≤ b * c ↔ a ≤ b) :=
  mul_comm c a ▸ mul_comm c b ▸ mul_le_mul_left
Right Multiplication Preserves Order in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $c \neq 0$ and $c \neq \infty$, the inequality $a \cdot c \leq b \cdot c$ holds if and only if $a \leq b$.
ENNReal.mul_lt_mul_left theorem
(h0 : a ≠ 0) (hinf : a ≠ ∞) : a * b < a * c ↔ b < c
Full source 
theorem mul_lt_mul_left (h0 : a ≠ 0) (hinf : a ≠ ∞) : a * b < a * c ↔ b < c :=
  (mul_left_strictMono h0 hinf).lt_iff_lt
Left Multiplication Preserves Strict Inequality in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $a \neq 0$ and $a \neq \infty$, the inequality $a \cdot b < a \cdot c$ holds if and only if $b < c$.
ENNReal.mul_lt_mul_right theorem
: c ≠ 0 → c ≠ ∞ → (a * c < b * c ↔ a < b)
Full source 
theorem mul_lt_mul_right : c ≠ 0 → c ≠ ∞ → (a * c < b * c ↔ a < b) :=
  mul_comm c a ▸ mul_comm c b ▸ mul_lt_mul_left
Right Multiplication Preserves Strict Inequality in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $c \neq 0$ and $c \neq \infty$, the inequality $a \cdot c < b \cdot c$ holds if and only if $a < b$.
ENNReal.mul_eq_left theorem
(ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * b = a ↔ b = 1
Full source 
protected lemma mul_eq_left (ha₀ : a ≠ 0) (ha : a ≠ ∞) : a * b = a ↔ b = 1 := by
  simpa using ENNReal.mul_right_inj ha₀ ha (c := 1)
Left Multiplication Identity Criterion in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $a \neq 0$ and $a \neq \infty$, the equality $a \cdot b = a$ holds if and only if $b = 1$.
ENNReal.mul_eq_right theorem
(hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b = b ↔ a = 1
Full source 
protected lemma mul_eq_right (hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b = b ↔ a = 1 := by
  simpa using ENNReal.mul_left_inj hb₀ hb (b := 1)
Right Multiplication Identity Criterion in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $b \neq 0$ and $b \neq \infty$, the equality $a \cdot b = b$ holds if and only if $a = 1$.
ENNReal.pow_pos theorem
: 0 < a → ∀ n : ℕ, 0 < a ^ n
Full source 
protected theorem pow_pos : 0 < a → ∀ n : ℕ, 0 < a ^ n :=
  CanonicallyOrderedAdd.pow_pos
Positivity of Powers in Extended Non-Negative Real Numbers
Informal description
For any extended non-negative real number $a$ such that $0 < a$, and for any natural number $n$, it holds that $0 < a^n$.
ENNReal.pow_ne_zero theorem
: a ≠ 0 → ∀ n : ℕ, a ^ n ≠ 0
Full source 
protected theorem pow_ne_zero : a ≠ 0 → ∀ n : ℕ, a ^ n ≠ 0 := by
  simpa only [pos_iff_ne_zero] using ENNReal.pow_pos
Non-Zero Property of Powers in Extended Non-Negative Real Numbers: $a \neq 0 \implies a^n \neq 0$
Informal description
For any extended non-negative real number $a$ such that $a \neq 0$, and for any natural number $n$, it holds that $a^n \neq 0$.
ENNReal.not_lt_zero theorem
: ¬a < 0
Full source 
theorem not_lt_zero : ¬a < 0 := by simp
Non-Negativity of Extended Real Numbers: $\neg(a < 0)$
Informal description
For any extended non-negative real number $a$, it is not true that $a < 0$.
ENNReal.le_of_add_le_add_left theorem
: a ≠ ∞ → a + b ≤ a + c → b ≤ c
Full source 
protected theorem le_of_add_le_add_left : a ≠ ∞ → a + b ≤ a + c → b ≤ c :=
  WithTop.le_of_add_le_add_left
Left Cancellation of Addition in Extended Non-Negative Real Numbers: $a \neq \infty \implies (a + b \leq a + c \to b \leq c)$
Informal description
For any extended non-negative real numbers $a$, $b$, and $c$, if $a$ is finite (i.e., $a \neq \infty$) and $a + b \leq a + c$, then $b \leq c$.
ENNReal.le_of_add_le_add_right theorem
: a ≠ ∞ → b + a ≤ c + a → b ≤ c
Full source 
protected theorem le_of_add_le_add_right : a ≠ ∞ → b + a ≤ c + a → b ≤ c :=
  WithTop.le_of_add_le_add_right
Right Cancellation of Addition in Extended Non-Negative Real Numbers: $a \neq \infty \implies (b + a \leq c + a \to b \leq c)$
Informal description
For any extended non-negative real numbers $a$, $b$, and $c$, if $a$ is finite (i.e., $a \neq \infty$) and $b + a \leq c + a$, then $b \leq c$.
ENNReal.add_lt_add_left theorem
: a ≠ ∞ → b < c → a + b < a + c
Full source 
@[gcongr] protected theorem add_lt_add_left : a ≠ ∞ → b < c → a + b < a + c :=
  WithTop.add_lt_add_left
Left Addition Preserves Strict Inequality in Extended Non-Negative Real Numbers
Informal description
For any extended non-negative real numbers $a$, $b$, and $c$, if $a$ is finite (i.e., $a \neq \infty$) and $b < c$, then $a + b < a + c$.
ENNReal.add_lt_add_right theorem
: a ≠ ∞ → b < c → b + a < c + a
Full source 
@[gcongr] protected theorem add_lt_add_right : a ≠ ∞ → b < c → b + a < c + a :=
  WithTop.add_lt_add_right
Right Addition Preserves Strict Inequality in Extended Non-Negative Real Numbers for Finite Addends
Informal description
For any extended non-negative real numbers $a$, $b$, and $c$, if $a$ is finite (i.e., $a \neq \infty$) and $b < c$, then $b + a < c + a$.
ENNReal.add_le_add_iff_left theorem
: a ≠ ∞ → (a + b ≤ a + c ↔ b ≤ c)
Full source 
protected theorem add_le_add_iff_left : a ≠ ∞ → (a + b ≤ a + c ↔ b ≤ c) :=
  WithTop.add_le_add_iff_left
Left Addition Preserves Inequality in Extended Non-Negative Real Numbers for Finite Addends
Informal description
For any extended non-negative real numbers $a$, $b$, and $c$, if $a$ is finite (i.e., $a \neq \infty$), then the inequality $a + b \leq a + c$ holds if and only if $b \leq c$.
ENNReal.add_le_add_iff_right theorem
: a ≠ ∞ → (b + a ≤ c + a ↔ b ≤ c)
Full source 
protected theorem add_le_add_iff_right : a ≠ ∞ → (b + a ≤ c + a ↔ b ≤ c) :=
  WithTop.add_le_add_iff_right
Right Addition Preserves Inequality in Extended Non-Negative Real Numbers for Finite Addends
Informal description
For any extended non-negative real numbers $b$ and $c$, and any finite extended non-negative real number $a$ (i.e., $a \neq \infty$), the inequality $b + a \leq c + a$ holds if and only if $b \leq c$.
ENNReal.add_lt_add_iff_left theorem
: a ≠ ∞ → (a + b < a + c ↔ b < c)
Full source 
protected theorem add_lt_add_iff_left : a ≠ ∞ → (a + b < a + c ↔ b < c) :=
  WithTop.add_lt_add_iff_left
Left Addition Preserves Strict Inequality in Extended Non-Negative Real Numbers for Finite Addends
Informal description
For any extended non-negative real numbers $b$ and $c$, and any finite extended non-negative real number $a$ (i.e., $a \neq \infty$), the strict inequality $a + b < a + c$ holds if and only if $b < c$.
ENNReal.add_lt_add_iff_right theorem
: a ≠ ∞ → (b + a < c + a ↔ b < c)
Full source 
protected theorem add_lt_add_iff_right : a ≠ ∞ → (b + a < c + a ↔ b < c) :=
  WithTop.add_lt_add_iff_right
Right Addition Preserves Strict Inequality in Extended Non-Negative Real Numbers for Finite Addends
Informal description
For any extended non-negative real numbers $b$ and $c$, and any finite extended non-negative real number $a$ (i.e., $a \neq \infty$), the strict inequality $b + a < c + a$ holds if and only if $b < c$.
ENNReal.add_lt_add_of_le_of_lt theorem
: a ≠ ∞ → a ≤ b → c < d → a + c < b + d
Full source 
protected theorem add_lt_add_of_le_of_lt : a ≠ ∞ → a ≤ b → c < d → a + c < b + d :=
  WithTop.add_lt_add_of_le_of_lt
Strict inequality preservation under addition with finite left term: $a \leq b$ and $c < d$ implies $a + c < b + d$ when $a \neq \infty$
Informal description
For any extended non-negative real numbers $a, b, c, d \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \neq \infty$, $a \leq b$, and $c < d$, then $a + c < b + d$.
ENNReal.add_lt_add_of_lt_of_le theorem
: c ≠ ∞ → a < b → c ≤ d → a + c < b + d
Full source 
protected theorem add_lt_add_of_lt_of_le : c ≠ ∞ → a < b → c ≤ d → a + c < b + d :=
  WithTop.add_lt_add_of_lt_of_le
Strict inequality preservation under addition with finite right term: $a < b$ and $c \leq d$ implies $a + c < b + d$ when $c \neq \infty$
Informal description
For extended non-negative real numbers $a, b, c, d \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $c \neq \infty$, $a < b$, and $c \leq d$, then $a + c < b + d$.
ENNReal.addLeftReflectLT instance
: AddLeftReflectLT ℝ≥0∞
Full source 
instance addLeftReflectLT : AddLeftReflectLT ℝ≥0∞ :=
  WithTop.addLeftReflectLT
Left Reflection Property of Addition on Extended Non-Negative Real Numbers
Informal description
The extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ satisfy the left reflection property for addition with respect to the strict order. That is, for any $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a + c < b + c$, then $a < b$.
ENNReal.lt_add_right theorem
(ha : a ≠ ∞) (hb : b ≠ 0) : a < a + b
Full source 
theorem lt_add_right (ha : a ≠ ∞) (hb : b ≠ 0) : a < a + b := by
  rwa [← pos_iff_ne_zero, ← ENNReal.add_lt_add_iff_left ha, add_zero] at hb
Strict Inequality Under Right Addition in Extended Non-Negative Reals
Informal description
For any finite extended non-negative real number $a$ (i.e., $a \neq \infty$) and any non-zero extended non-negative real number $b$ (i.e., $b \neq 0$), it holds that $a < a + b$.
ENNReal.add_eq_top theorem
: a + b = ∞ ↔ a = ∞ ∨ b = ∞
Full source 
@[simp] theorem add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := WithTop.add_eq_top
Sum Equals Infinity in Extended Non-Negative Reals if and Only if One Term is Infinity
Informal description
For extended non-negative real numbers $a$ and $b$, the sum $a + b$ equals infinity if and only if either $a$ is infinity or $b$ is infinity, i.e., $a + b = \infty \leftrightarrow (a = \infty \lor b = \infty)$.
ENNReal.add_lt_top theorem
: a + b < ∞ ↔ a < ∞ ∧ b < ∞
Full source 
@[simp] theorem add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := WithTop.add_lt_top
Sum of Extended Non-Negative Reals is Finite if and Only if Both Terms are Finite
Informal description
For extended non-negative real numbers $a$ and $b$, the sum $a + b$ is finite if and only if both $a$ and $b$ are finite, i.e., $a + b < \infty \leftrightarrow (a < \infty \land b < \infty)$.
ENNReal.toNNReal_add theorem
{r₁ r₂ : ℝ≥0∞} (h₁ : r₁ ≠ ∞) (h₂ : r₂ ≠ ∞) : (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal
Full source 
theorem toNNReal_add {r₁ r₂ : ℝ≥0∞} (h₁ : r₁ ≠ ∞) (h₂ : r₂ ≠ ∞) :
    (r₁ + r₂).toNNReal = r₁.toNNReal + r₂.toNNReal := by
  lift r₁ to ℝ≥0 using h₁
  lift r₂ to ℝ≥0 using h₂
  rfl
Additivity of the Canonical Map from Extended Non-Negative Reals to Non-Negative Reals
Informal description
For any extended non-negative real numbers $r₁$ and $r₂$ such that $r₁ \neq \infty$ and $r₂ \neq \infty$, the canonical map to non-negative real numbers satisfies $(r₁ + r₂).\text{toNNReal} = r₁.\text{toNNReal} + r₂.\text{toNNReal}$.
ENNReal.toReal_le_add' theorem
(hle : a ≤ b + c) (hb : b = ∞ → a = ∞) (hc : c = ∞ → a = ∞) : a.toReal ≤ b.toReal + c.toReal
Full source 
/-- If `a ≤ b + c` and `a = ∞` whenever `b = ∞` or `c = ∞`, then
`ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c`. This lemma is useful to transfer
triangle-like inequalities from `ENNReal`s to `Real`s. -/
theorem toReal_le_add' (hle : a ≤ b + c) (hb : b = ∞ → a = ∞) (hc : c = ∞ → a = ∞) :
    a.toReal ≤ b.toReal + c.toReal := by
  refine le_trans (toReal_mono' hle ?_) toReal_add_le
  simpa only [add_eq_top, or_imp] using And.intro hb hc
Triangle Inequality for Real Projection of Extended Non-Negative Reals with Infinity Conditions
Informal description
For extended non-negative real numbers $a$, $b$, and $c$, if $a \leq b + c$ and $a = \infty$ whenever either $b = \infty$ or $c = \infty$, then the real-valued projection satisfies $a.\text{toReal} \leq b.\text{toReal} + c.\text{toReal}$.
ENNReal.toReal_le_add theorem
(hle : a ≤ b + c) (hb : b ≠ ∞) (hc : c ≠ ∞) : a.toReal ≤ b.toReal + c.toReal
Full source 
/-- If `a ≤ b + c`, `b ≠ ∞`, and `c ≠ ∞`, then
`ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c`. This lemma is useful to transfer
triangle-like inequalities from `ENNReal`s to `Real`s. -/
theorem toReal_le_add (hle : a ≤ b + c) (hb : b ≠ ∞) (hc : c ≠ ∞) :
    a.toReal ≤ b.toReal + c.toReal :=
  toReal_le_add' hle (flip absurd hb) (flip absurd hc)
Triangle Inequality for Real Projection of Extended Non-Negative Reals
Informal description
For extended non-negative real numbers $a$, $b$, and $c$, if $a \leq b + c$ and both $b$ and $c$ are finite (i.e., $b \neq \infty$ and $c \neq \infty$), then the real-valued projections satisfy $a_{\text{toReal}} \leq b_{\text{toReal}} + c_{\text{toReal}}$.
ENNReal.not_lt_top theorem
{x : ℝ≥0∞} : ¬x < ∞ ↔ x = ∞
Full source 
theorem not_lt_top {x : ℝ≥0∞} : ¬x < ∞¬x < ∞ ↔ x = ∞ := by rw [lt_top_iff_ne_top, Classical.not_not]
Characterization of Non-Strictly-Less-Than-Infinity in Extended Non-Negative Reals: $\neg (x < \infty) \leftrightarrow x = \infty$
Informal description
For any extended non-negative real number $x$, it is not the case that $x$ is strictly less than infinity if and only if $x$ equals infinity, i.e., $\neg (x < \infty) \leftrightarrow x = \infty$.
ENNReal.add_ne_top theorem
: a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞
Full source 
theorem add_ne_top : a + b ≠ ∞a + b ≠ ∞ ↔ a ≠ ∞ ∧ b ≠ ∞ := by simpa only [lt_top_iff_ne_top] using add_lt_top
Sum of Extended Non-Negative Reals is Finite if and Only if Both Terms are Finite
Informal description
For extended non-negative real numbers $a$ and $b$, the sum $a + b$ is not equal to infinity if and only if both $a$ and $b$ are not equal to infinity, i.e., $a + b \neq \infty \leftrightarrow (a \neq \infty \land b \neq \infty)$.
ENNReal.Finiteness.add_ne_top theorem
{a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) : a + b ≠ ∞
Full source 
@[aesop (rule_sets := [finiteness]) safe apply]
protected lemma Finiteness.add_ne_top {a b : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≠ ∞) : a + b ≠ ∞ :=
  ENNReal.add_ne_top.2 ⟨ha, hb⟩
Finite Sum of Finite Extended Non-Negative Reals is Finite
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, their sum $a + b$ is also not equal to infinity.
ENNReal.mul_top' theorem
: a * ∞ = if a = 0 then 0 else ∞
Full source 
theorem mul_top' : a * ∞ = if a = 0 then 0 else ∞ := by convert WithTop.mul_top' a
Multiplication by Infinity in Extended Non-Negative Reals: $a \cdot \infty = \text{if } a = 0 \text{ then } 0 \text{ else } \infty$
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product $a \cdot \infty$ equals $0$ if $a = 0$, and equals $\infty$ otherwise.
ENNReal.mul_top theorem
(h : a ≠ 0) : a * ∞ = ∞
Full source 
@[simp] theorem mul_top (h : a ≠ 0) : a * ∞ = ∞ := WithTop.mul_top h
Multiplication of Nonzero Extended Non-Negative Real by Infinity Yields Infinity
Informal description
For any nonzero extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product $a \cdot \infty$ equals $\infty$.
ENNReal.top_mul' theorem
: ∞ * a = if a = 0 then 0 else ∞
Full source 
theorem top_mul' : ∞ * a = if a = 0 then 0 else ∞ := by convert WithTop.top_mul' a
Multiplication of Infinity in Extended Non-Negative Reals: $\infty \cdot a = \text{if } a = 0 \text{ then } 0 \text{ else } \infty$
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product $\infty \cdot a$ equals $0$ if $a = 0$, and equals $\infty$ otherwise.
ENNReal.top_mul theorem
(h : a ≠ 0) : ∞ * a = ∞
Full source 
@[simp] theorem top_mul (h : a ≠ 0) : ∞ * a = ∞ := WithTop.top_mul h
Multiplication of Infinity by Nonzero Extended Non-Negative Real Yields Infinity
Informal description
For any nonzero extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the product $\infty \cdot a$ equals $\infty$.
ENNReal.top_mul_top theorem
: ∞ * ∞ = ∞
Full source 
theorem top_mul_top : ∞ * ∞ = ∞ := WithTop.top_mul_top
Product of Infinity with Itself in Extended Non-Negative Reals
Informal description
The product of the extended non-negative real number infinity with itself is infinity, i.e., $\infty \cdot \infty = \infty$.
ENNReal.mul_eq_top theorem
: a * b = ∞ ↔ a ≠ 0 ∧ b = ∞ ∨ a = ∞ ∧ b ≠ 0
Full source 
theorem mul_eq_top : a * b = ∞ ↔ a ≠ 0 ∧ b = ∞ ∨ a = ∞ ∧ b ≠ 0 :=
  WithTop.mul_eq_top_iff
Product Equals Infinity in Extended Non-Negative Reals if and only if One Factor is Infinity and the Other is Nonzero
Informal description
For any extended non-negative real numbers $a$ and $b$, the product $a \cdot b$ equals $\infty$ if and only if either $a \neq 0$ and $b = \infty$, or $a = \infty$ and $b \neq 0$.
ENNReal.mul_lt_top theorem
: a < ∞ → b < ∞ → a * b < ∞
Full source 
theorem mul_lt_top : a < ∞ → b < ∞ → a * b < ∞ := WithTop.mul_lt_top
Finite Extended Non-Negative Reals Have Finite Product
Informal description
For any extended non-negative real numbers $a$ and $b$, if $a < \infty$ and $b < \infty$, then their product satisfies $a \cdot b < \infty$.
ENNReal.mul_ne_top theorem
: a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞
Full source 
@[aesop (rule_sets := [finiteness]) unsafe 75% apply]
theorem mul_ne_top : a ≠ ∞ → b ≠ ∞ → a * b ≠ ∞ := WithTop.mul_ne_top
Product of Finite Extended Non-Negative Reals is Finite
Informal description
For any extended non-negative real numbers $a$ and $b$, if $a \neq \infty$ and $b \neq \infty$, then their product $a \cdot b \neq \infty$.
ENNReal.lt_top_of_mul_ne_top_right theorem
(h : a * b ≠ ∞) (ha : a ≠ 0) : b < ∞
Full source 
theorem lt_top_of_mul_ne_top_right (h : a * b ≠ ∞) (ha : a ≠ 0) : b < ∞ :=
  lt_top_of_mul_ne_top_left (by rwa [mul_comm]) ha
Finite Right Factor in Nonzero Product of Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$, if the product $a \cdot b \neq \infty$ and $a \neq 0$, then $b < \infty$.
ENNReal.mul_lt_top_iff theorem
{a b : ℝ≥0∞} : a * b < ∞ ↔ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0
Full source 
theorem mul_lt_top_iff {a b : ℝ≥0∞} : a * b < ∞ ↔ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0 := by
  constructor
  · intro h
    rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]
    intro hb ha
    exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩
  · rintro (⟨ha, hb⟩ | rfl | rfl) <;> [exact mul_lt_top ha hb; simp; simp]
Finite Product Criterion for Extended Non-Negative Reals: $a \cdot b < \infty \leftrightarrow (a < \infty \land b < \infty) \lor a = 0 \lor b = 0$
Informal description
For any extended non-negative real numbers $a$ and $b$, the product $a \cdot b$ is finite if and only if either both $a$ and $b$ are finite, or at least one of them is zero. In other words, $a \cdot b < \infty \leftrightarrow (a < \infty \land b < \infty) \lor (a = 0) \lor (b = 0)$.
ENNReal.mul_self_lt_top_iff theorem
{a : ℝ≥0∞} : a * a < ⊤ ↔ a < ⊤
Full source 
theorem mul_self_lt_top_iff {a : ℝ≥0∞} : a * a < ⊤ ↔ a < ⊤ := by
  rw [ENNReal.mul_lt_top_iff, and_self, or_self, or_iff_left_iff_imp]
  rintro rfl
  exact zero_lt_top
Square Finiteness Criterion for Extended Non-Negative Reals: $a^2 < \infty \leftrightarrow a < \infty$
Informal description
For any extended non-negative real number $a$, the product $a \cdot a$ is finite if and only if $a$ is finite, i.e., $a \cdot a < \infty \leftrightarrow a < \infty$.
ENNReal.mul_pos_iff theorem
: 0 < a * b ↔ 0 < a ∧ 0 < b
Full source 
theorem mul_pos_iff : 0 < a * b ↔ 0 < a ∧ 0 < b :=
  CanonicallyOrderedAdd.mul_pos
Positivity of Product in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$, the product $a \cdot b$ is strictly positive if and only if both $a$ and $b$ are strictly positive. In other words, $0 < a \cdot b \leftrightarrow (0 < a) \land (0 < b)$.
ENNReal.mul_pos theorem
(ha : a ≠ 0) (hb : b ≠ 0) : 0 < a * b
Full source 
theorem mul_pos (ha : a ≠ 0) (hb : b ≠ 0) : 0 < a * b :=
  mul_pos_iff.2 ⟨pos_iff_ne_zero.2 ha, pos_iff_ne_zero.2 hb⟩
Positivity of Nonzero Product in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq 0$ and $b \neq 0$, the product $a \cdot b$ is strictly positive, i.e., $0 < a \cdot b$.
ENNReal.top_pow theorem
{n : ℕ} (hn : n ≠ 0) : (∞ : ℝ≥0∞) ^ n = ∞
Full source 
@[simp] lemma top_pow {n : ℕ} (hn : n ≠ 0) : (∞ : ℝ≥0∞) ^ n = ∞ := WithTop.top_pow hn
Power of Infinity in Extended Non-Negative Reals: $\infty^n = \infty$ for $n \neq 0$
Informal description
For any natural number $n \neq 0$, the $n$-th power of the infinity element $\infty$ in the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals $\infty$, i.e., $\infty^n = \infty$.
ENNReal.pow_eq_top_iff theorem
: a ^ n = ∞ ↔ a = ∞ ∧ n ≠ 0
Full source 
@[simp] lemma pow_eq_top_iff : a ^ n = ∞ ↔ a = ∞ ∧ n ≠ 0 := WithTop.pow_eq_top_iff
Power Equals Infinity Condition in Extended Non-Negative Reals: $a^n = \infty \leftrightarrow a = \infty \land n \neq 0$
Informal description
For any extended non-negative real number $a$ and natural number $n$, the power $a^n$ equals infinity if and only if $a = \infty$ and $n \neq 0$. In other words, $a^n = \infty \leftrightarrow (a = \infty \land n \neq 0)$.
ENNReal.pow_ne_top_iff theorem
: a ^ n ≠ ∞ ↔ a ≠ ∞ ∨ n = 0
Full source 
lemma pow_ne_top_iff : a ^ n ≠ ∞a ^ n ≠ ∞ ↔ a ≠ ∞ ∨ n = 0 := WithTop.pow_ne_top_iff
Non-infinity Power Condition in Extended Non-Negative Reals: $a^n \neq \infty \leftrightarrow a \neq \infty \lor n = 0$
Informal description
For any extended non-negative real number $a$ and natural number $n$, the power $a^n$ is not equal to infinity if and only if either $a$ is not equal to infinity or $n$ is zero. In other words, $a^n \neq \infty \leftrightarrow a \neq \infty \lor n = 0$.
ENNReal.pow_lt_top_iff theorem
: a ^ n < ∞ ↔ a < ∞ ∨ n = 0
Full source 
@[simp] lemma pow_lt_top_iff : a ^ n < ∞ ↔ a < ∞ ∨ n = 0 := WithTop.pow_lt_top_iff
Power Strictly Less Than Infinity in Extended Non-Negative Reals
Informal description
For any extended non-negative real number $a$ and natural number $n$, the power $a^n$ is strictly less than infinity if and only if either $a$ is strictly less than infinity or $n$ is zero. In other words, $a^n < \infty \leftrightarrow a < \infty \lor n = 0$.
ENNReal.pow_ne_top theorem
(ha : a ≠ ∞) : a ^ n ≠ ∞
Full source 
lemma pow_ne_top (ha : a ≠ ∞) : a ^ n ≠ ∞ := WithTop.pow_ne_top ha
Finite Extended Reals Have Finite Powers
Informal description
For any extended non-negative real number $a \neq \infty$ and any natural number $n$, the power $a^n$ is not equal to $\infty$.
ENNReal.pow_lt_top theorem
(ha : a < ∞) : a ^ n < ∞
Full source 
lemma pow_lt_top (ha : a < ∞) : a ^ n < ∞ := WithTop.pow_lt_top ha
Finite Powers Remain Finite in Extended Non-Negative Reals
Informal description
For any extended non-negative real number $a$ such that $a < \infty$ and any natural number $n$, the power $a^n$ is strictly less than $\infty$.
ENNReal.add_lt_add theorem
(ac : a < c) (bd : b < d) : a + b < c + d
Full source 
@[gcongr] protected theorem add_lt_add (ac : a < c) (bd : b < d) : a + b < c + d := by
  lift a to ℝ≥0 using ac.ne_top
  lift b to ℝ≥0 using bd.ne_top
  cases c; · simp
  cases d; · simp
  simp only [← coe_add, some_eq_coe, coe_lt_coe] at *
  exact add_lt_add ac bd
Strict Inequality Preservation under Addition in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b, c, d$ such that $a < c$ and $b < d$, the sum $a + b$ is strictly less than $c + d$.
ENNReal.addLECancellable_iff_ne theorem
{a : ℝ≥0∞} : AddLECancellable a ↔ a ≠ ∞
Full source 
/-- An element `a` is `AddLECancellable` if `a + b ≤ a + c` implies `b ≤ c` for all `b` and `c`.
  This is true in `ℝ≥0∞` for all elements except `∞`. -/
@[simp]
theorem addLECancellable_iff_ne {a : ℝ≥0∞} : AddLECancellableAddLECancellable a ↔ a ≠ ∞ := by
  constructor
  · rintro h rfl
    refine zero_lt_one.not_le (h ?_)
    simp
  · rintro h b c hbc
    apply ENNReal.le_of_add_le_add_left h hbc
Characterization of Additive Left Cancellability in Extended Non-Negative Reals: $a$ is cancellable $\iff$ $a \neq \infty$
Informal description
An extended non-negative real number $a$ is additively left cancellable (i.e., $a + b \leq a + c$ implies $b \leq c$ for all $b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$) if and only if $a$ is not equal to $\infty$.
ENNReal.cancel_of_ne theorem
{a : ℝ≥0∞} (h : a ≠ ∞) : AddLECancellable a
Full source 
/-- This lemma has an abbreviated name because it is used frequently. -/
theorem cancel_of_ne {a : ℝ≥0∞} (h : a ≠ ∞) : AddLECancellable a :=
  addLECancellable_iff_ne.mpr h
Finite Extended Non-Negative Reals are Additively Left Cancellable
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \neq \infty$, then $a$ is additively left cancellable (i.e., for all $b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a + b \leq a + c$ implies $b \leq c$).
ENNReal.cancel_of_lt theorem
{a : ℝ≥0∞} (h : a < ∞) : AddLECancellable a
Full source 
/-- This lemma has an abbreviated name because it is used frequently. -/
theorem cancel_of_lt {a : ℝ≥0∞} (h : a < ∞) : AddLECancellable a :=
  cancel_of_ne h.ne
Additive Left Cancellability for Finite Extended Non-Negative Reals
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a$ is strictly less than $\infty$, then $a$ is additively left cancellable (i.e., for all $b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a + b \leq a + c$ implies $b \leq c$).
ENNReal.cancel_of_lt' theorem
{a b : ℝ≥0∞} (h : a < b) : AddLECancellable a
Full source 
/-- This lemma has an abbreviated name because it is used frequently. -/
theorem cancel_of_lt' {a b : ℝ≥0∞} (h : a < b) : AddLECancellable a :=
  cancel_of_ne h.ne_top
Additive Left Cancellability for Finite Extended Non-Negative Reals Under Strict Inequality
Informal description
For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a < b$, then $a$ is additively left cancellable (i.e., for all $c, d \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a + c \leq a + d$ implies $c \leq d$).
ENNReal.cancel_coe theorem
{a : ℝ≥0} : AddLECancellable (a : ℝ≥0∞)
Full source 
/-- This lemma has an abbreviated name because it is used frequently. -/
theorem cancel_coe {a : ℝ≥0} : AddLECancellable (a : ℝ≥0∞) :=
  cancel_of_ne coe_ne_top
Additive Left Cancellation for Coerced Non-Negative Reals in Extended Non-Negative Reals
Informal description
For any non-negative real number $a \in \mathbb{R}_{\geq 0}$, the extended non-negative real number obtained by coercing $a$ to $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is additively left cancellable (i.e., for all $b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the inequality $a + b \leq a + c$ implies $b \leq c$).
ENNReal.add_right_inj theorem
(h : a ≠ ∞) : a + b = a + c ↔ b = c
Full source 
theorem add_right_inj (h : a ≠ ∞) : a + b = a + c ↔ b = c :=
  (cancel_of_ne h).inj
Right Cancellation Law for Addition in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \neq \infty$, then the equality $a + b = a + c$ holds if and only if $b = c$.
ENNReal.add_left_inj theorem
(h : a ≠ ∞) : b + a = c + a ↔ b = c
Full source 
theorem add_left_inj (h : a ≠ ∞) : b + a = c + a ↔ b = c :=
  (cancel_of_ne h).inj_left
Left Cancellation of Finite Extended Non-Negative Reals in Addition
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \neq \infty$, then $b + a = c + a$ if and only if $b = c$.
ENNReal.sub_eq_sInf theorem
{a b : ℝ≥0∞} : a - b = sInf {d | a ≤ d + b}
Full source 
theorem sub_eq_sInf {a b : ℝ≥0∞} : a - b = sInf { d | a ≤ d + b } :=
  le_antisymm (le_sInf fun _ h => tsub_le_iff_right.mpr h) <| sInf_le <| mem_setOf.2 le_tsub_add
Truncated Subtraction as Infimum in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$, the truncated subtraction $a - b$ is equal to the infimum of the set $\{d \mid a \leq d + b\}$.
ENNReal.coe_sub theorem
: (↑(r - p) : ℝ≥0∞) = ↑r - ↑p
Full source 
/-- This is a special case of `WithTop.coe_sub` in the `ENNReal` namespace -/
@[simp, norm_cast] theorem coe_sub : (↑(r - p) : ℝ≥0∞) = ↑r - ↑p := WithTop.coe_sub
Embedding Preserves Subtraction in Extended Non-Negative Reals
Informal description
For any two non-negative real numbers $r$ and $p$, the canonical embedding of their difference $r - p$ into the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the difference of their embeddings, i.e., $(r - p : \mathbb{R}_{\geq 0} \cup \{\infty\}) = (r : \mathbb{R}_{\geq 0} \cup \{\infty\}) - (p : \mathbb{R}_{\geq 0} \cup \{\infty\})$.
ENNReal.top_sub_coe theorem
: ∞ - ↑r = ∞
Full source 
/-- This is a special case of `WithTop.top_sub_coe` in the `ENNReal` namespace -/
@[simp] theorem top_sub_coe : ∞ - ↑r = ∞ := WithTop.top_sub_coe
Subtraction from Infinity in Extended Non-Negative Reals: $\infty - r = \infty$
Informal description
For any non-negative real number $r$, the difference $\infty - r$ in the extended non-negative real numbers equals $\infty$.
ENNReal.top_sub theorem
(ha : a ≠ ∞) : ∞ - a = ∞
Full source 
@[simp] lemma top_sub (ha : a ≠ ∞) : ∞ - a = ∞ := by lift a to ℝ≥0 using ha; exact top_sub_coe
Subtraction from Infinity in Extended Non-Negative Reals: $\infty - a = \infty$ when $a \neq \infty$
Informal description
For any extended non-negative real number $a$ such that $a \neq \infty$, the difference $\infty - a$ equals $\infty$.
ENNReal.sub_top theorem
: a - ∞ = 0
Full source 
/-- This is a special case of `WithTop.sub_top` in the `ENNReal` namespace -/
theorem sub_top : a - ∞ = 0 := WithTop.sub_top
Subtraction of Infinity in Extended Non-Negative Reals: $a - \infty = 0$
Informal description
For any extended non-negative real number $a$, the difference $a - \infty$ equals $0$.
ENNReal.sub_eq_top_iff theorem
: a - b = ∞ ↔ a = ∞ ∧ b ≠ ∞
Full source 
@[simp] theorem sub_eq_top_iff : a - b = ∞ ↔ a = ∞ ∧ b ≠ ∞ := WithTop.sub_eq_top_iff
Difference Equals Infinity in Extended Non-Negative Reals: $a - b = \infty \iff (a = \infty \land b \neq \infty)$
Informal description
For extended non-negative real numbers $a$ and $b$, the difference $a - b$ equals $\infty$ if and only if $a = \infty$ and $b \neq \infty$.
ENNReal.sub_ne_top_iff theorem
: a - b ≠ ∞ ↔ a ≠ ∞ ∨ b = ∞
Full source 
lemma sub_ne_top_iff : a - b ≠ ∞a - b ≠ ∞ ↔ a ≠ ∞ ∨ b = ∞ := WithTop.sub_ne_top_iff
Characterization of Finite Difference in Extended Non-Negative Real Numbers: $a - b \neq \infty \iff (a \neq \infty \lor b = \infty)$
Informal description
For extended non-negative real numbers $a$ and $b$, the difference $a - b$ is not equal to $\infty$ if and only if either $a$ is not equal to $\infty$ or $b$ is equal to $\infty$.
ENNReal.sub_ne_top theorem
(ha : a ≠ ∞) : a - b ≠ ∞
Full source 
@[aesop (rule_sets := [finiteness]) unsafe 75% apply]
theorem sub_ne_top (ha : a ≠ ∞) : a - b ≠ ∞ := mt sub_eq_top_iff.mp <| mt And.left ha
Finite Difference Property for Extended Non-Negative Reals: $a \neq \infty \implies a - b \neq \infty$
Informal description
For any extended non-negative real numbers $a$ and $b$, if $a \neq \infty$, then the difference $a - b$ is not equal to $\infty$.
ENNReal.natCast_sub theorem
(m n : ℕ) : ↑(m - n) = (m - n : ℝ≥0∞)
Full source 
@[simp, norm_cast]
theorem natCast_sub (m n : ℕ) : ↑(m - n) = (m - n : ℝ≥0∞) := by
  rw [← coe_natCast, Nat.cast_tsub, coe_sub, coe_natCast, coe_natCast]
Embedding Preserves Subtraction of Natural Numbers in Extended Non-Negative Reals
Informal description
For any natural numbers $m$ and $n$, the canonical embedding of their difference $m - n$ into the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ equals the difference of their embeddings, i.e., $(m - n : \mathbb{R}_{\geq 0} \cup \{\infty\}) = (m : \mathbb{R}_{\geq 0} \cup \{\infty\}) - (n : \mathbb{R}_{\geq 0} \cup \{\infty\})$.
ENNReal.sub_eq_of_eq_add theorem
(hb : b ≠ ∞) : a = c + b → a - b = c
Full source 
/-- See `ENNReal.sub_eq_of_eq_add'` for a version assuming that `a = c + b` itself is finite rather
than `b`. -/
protected theorem sub_eq_of_eq_add (hb : b ≠ ∞) : a = c + b → a - b = c :=
  (cancel_of_ne hb).tsub_eq_of_eq_add
Subtraction from Extended Non-Negative Reals under Finite Addend Condition
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $b \neq \infty$ and $a = c + b$, then $a - b = c$.
ENNReal.sub_eq_of_eq_add' theorem
(ha : a ≠ ∞) : a = c + b → a - b = c
Full source 
/-- Weaker version of `ENNReal.sub_eq_of_eq_add` assuming that `a = c + b` itself is finite rather
han `b`. -/
protected lemma sub_eq_of_eq_add' (ha : a ≠ ∞) : a = c + b → a - b = c :=
  (cancel_of_ne ha).tsub_eq_of_eq_add'
Subtraction from Finite Extended Non-Negative Reals under Additive Equality
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \neq \infty$ and $a = c + b$, then $a - b = c$.
ENNReal.sub_eq_of_eq_add_rev theorem
(hb : b ≠ ∞) : a = b + c → a - b = c
Full source 
/-- See `ENNReal.sub_eq_of_eq_add_rev'` for a version assuming that `a = b + c` itself is finite
rather than `b`. -/
protected theorem sub_eq_of_eq_add_rev (hb : b ≠ ∞) : a = b + c → a - b = c :=
  (cancel_of_ne hb).tsub_eq_of_eq_add_rev
Subtraction identity for extended non-negative reals: $a = b + c \Rightarrow a - b = c$ when $b \neq \infty$
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $b \neq \infty$ and $a = b + c$, then $a - b = c$.
ENNReal.sub_eq_of_eq_add_rev' theorem
(ha : a ≠ ∞) : a = b + c → a - b = c
Full source 
/-- Weaker version of `ENNReal.sub_eq_of_eq_add_rev` assuming that `a = b + c` itself is finite
rather than `b`. -/
protected lemma sub_eq_of_eq_add_rev' (ha : a ≠ ∞) : a = b + c → a - b = c :=
  (cancel_of_ne ha).tsub_eq_of_eq_add_rev'
Subtraction identity for finite extended non-negative reals: $a = b + c \implies a - b = c$ when $a \neq \infty$
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \neq \infty$ and $a = b + c$, then $a - b = c$.
ENNReal.add_sub_cancel_left theorem
(ha : a ≠ ∞) : a + b - a = b
Full source 
@[simp]
protected theorem add_sub_cancel_left (ha : a ≠ ∞) : a + b - a = b :=
  (cancel_of_ne ha).add_tsub_cancel_left
Left Cancellation of Addition and Subtraction for Finite Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $a \neq \infty$, the equality $(a + b) - a = b$ holds.
ENNReal.add_sub_cancel_right theorem
(hb : b ≠ ∞) : a + b - b = a
Full source 
@[simp]
protected theorem add_sub_cancel_right (hb : b ≠ ∞) : a + b - b = a :=
  (cancel_of_ne hb).add_tsub_cancel_right
Right Cancellation of Addition and Subtraction in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $b \neq \infty$, then $(a + b) - b = a$.
ENNReal.sub_add_eq_add_sub theorem
(hab : b ≤ a) (b_ne_top : b ≠ ∞) : a - b + c = a + c - b
Full source 
protected theorem sub_add_eq_add_sub (hab : b ≤ a) (b_ne_top : b ≠ ∞) :
    a - b + c = a + c - b := by
  by_cases c_top : c = ∞
  · simpa [c_top] using ENNReal.eq_sub_of_add_eq b_ne_top rfl
  refine ENNReal.eq_sub_of_add_eq b_ne_top ?_
  simp only [add_assoc, add_comm c b]
  simpa only [← add_assoc] using (add_left_inj c_top).mpr <| tsub_add_cancel_of_le hab
Subtraction-Additive Commutativity for Extended Non-Negative Reals
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $b \leq a$ and $b \neq \infty$, the equality $(a - b) + c = (a + c) - b$ holds.
ENNReal.lt_add_of_sub_lt_left theorem
(h : a ≠ ∞ ∨ b ≠ ∞) : a - b < c → a < b + c
Full source 
protected theorem lt_add_of_sub_lt_left (h : a ≠ ∞a ≠ ∞ ∨ b ≠ ∞) : a - b < c → a < b + c := by
  obtain rfl | hb := eq_or_ne b ∞
  · rw [top_add, lt_top_iff_ne_top]
    exact fun _ => h.resolve_right (Classical.not_not.2 rfl)
  · exact (cancel_of_ne hb).lt_add_of_tsub_lt_left
Inequality for Extended Non-Negative Reals: $a - b < c \to a < b + c$ when $a$ or $b$ is finite
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if either $a \neq \infty$ or $b \neq \infty$, then $a - b < c$ implies $a < b + c$.
ENNReal.lt_add_of_sub_lt_right theorem
(h : a ≠ ∞ ∨ c ≠ ∞) : a - c < b → a < b + c
Full source 
protected theorem lt_add_of_sub_lt_right (h : a ≠ ∞a ≠ ∞ ∨ c ≠ ∞) : a - c < b → a < b + c :=
  add_comm c b ▸ ENNReal.lt_add_of_sub_lt_left h
Inequality for Extended Non-Negative Reals: $a - c < b \to a < b + c$ when $a$ or $c$ is finite
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if either $a \neq \infty$ or $c \neq \infty$, then $a - c < b$ implies $a < b + c$.
ENNReal.le_sub_of_add_le_left theorem
(ha : a ≠ ∞) : a + b ≤ c → b ≤ c - a
Full source 
theorem le_sub_of_add_le_left (ha : a ≠ ∞) : a + b ≤ c → b ≤ c - a :=
  (cancel_of_ne ha).le_tsub_of_add_le_left
Subtraction Lower Bound from Left Addition Inequality in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \neq \infty$ and $a + b \leq c$, then $b \leq c - a$.
ENNReal.le_sub_of_add_le_right theorem
(hb : b ≠ ∞) : a + b ≤ c → a ≤ c - b
Full source 
theorem le_sub_of_add_le_right (hb : b ≠ ∞) : a + b ≤ c → a ≤ c - b :=
  (cancel_of_ne hb).le_tsub_of_add_le_right
Subtraction Inequality for Extended Non-Negative Reals with Finite Right Term
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $b \neq \infty$ and $a + b \leq c$, then $a \leq c - b$.
ENNReal.sub_lt_of_lt_add theorem
(hac : c ≤ a) (h : a < b + c) : a - c < b
Full source 
protected theorem sub_lt_of_lt_add (hac : c ≤ a) (h : a < b + c) : a - c < b :=
  ((cancel_of_lt' <| hac.trans_lt h).tsub_lt_iff_right hac).mpr h
Subtraction Inequality for Extended Non-Negative Reals under Addition Bound
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $c \leq a$ and $a < b + c$, then $a - c < b$.
ENNReal.sub_lt_iff_lt_right theorem
(hb : b ≠ ∞) (hab : b ≤ a) : a - b < c ↔ a < c + b
Full source 
protected theorem sub_lt_iff_lt_right (hb : b ≠ ∞) (hab : b ≤ a) : a - b < c ↔ a < c + b :=
  (cancel_of_ne hb).tsub_lt_iff_right hab
Subtraction-Inequality Equivalence for Extended Non-Negative Reals
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $b \neq \infty$ and $b \leq a$, the inequality $a - b < c$ holds if and only if $a < c + b$.
ENNReal.sub_lt_self theorem
(ha : a ≠ ∞) (ha₀ : a ≠ 0) (hb : b ≠ 0) : a - b < a
Full source 
protected theorem sub_lt_self (ha : a ≠ ∞) (ha₀ : a ≠ 0) (hb : b ≠ 0) : a - b < a :=
  (cancel_of_ne ha).tsub_lt_self (pos_iff_ne_zero.2 ha₀) (pos_iff_ne_zero.2 hb)
Strict Inequality for Nonzero Truncated Subtraction in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a$ is finite and nonzero ($a \neq \infty$ and $a \neq 0$) and $b$ is nonzero ($b \neq 0$), then $a - b < a$.
ENNReal.sub_lt_self_iff theorem
(ha : a ≠ ∞) : a - b < a ↔ 0 < a ∧ 0 < b
Full source 
protected theorem sub_lt_self_iff (ha : a ≠ ∞) : a - b < a ↔ 0 < a ∧ 0 < b :=
  (cancel_of_ne ha).tsub_lt_self_iff
Inequality for Truncated Subtraction in Extended Non-Negative Reals: $a - b < a \leftrightarrow a > 0 \land b > 0$
Informal description
For any extended non-negative real number $a \neq \infty$, the inequality $a - b < a$ holds if and only if $a > 0$ and $b > 0$.
ENNReal.sub_lt_of_sub_lt theorem
(h₂ : c ≤ a) (h₃ : a ≠ ∞ ∨ b ≠ ∞) (h₁ : a - b < c) : a - c < b
Full source 
theorem sub_lt_of_sub_lt (h₂ : c ≤ a) (h₃ : a ≠ ∞a ≠ ∞ ∨ b ≠ ∞) (h₁ : a - b < c) : a - c < b :=
  ENNReal.sub_lt_of_lt_add h₂ (add_comm c b ▸ ENNReal.lt_add_of_sub_lt_right h₃ h₁)
Subtraction Inequality for Extended Non-Negative Reals: $a - b < c \to a - c < b$ under finiteness conditions
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $c \leq a$, either $a \neq \infty$ or $b \neq \infty$, and $a - b < c$, then $a - c < b$.
ENNReal.sub_sub_cancel theorem
(h : a ≠ ∞) (h2 : b ≤ a) : a - (a - b) = b
Full source 
theorem sub_sub_cancel (h : a ≠ ∞) (h2 : b ≤ a) : a - (a - b) = b :=
  (cancel_of_ne <| sub_ne_top h).tsub_tsub_cancel_of_le h2
Double Subtraction Cancellation in Extended Non-Negative Reals: $a - (a - b) = b$ when $a \neq \infty$ and $b \leq a$
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \leq a$, the double subtraction $a - (a - b)$ equals $b$.
ENNReal.sub_right_inj theorem
{a b c : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≤ a) (hc : c ≤ a) : a - b = a - c ↔ b = c
Full source 
theorem sub_right_inj {a b c : ℝ≥0∞} (ha : a ≠ ∞) (hb : b ≤ a) (hc : c ≤ a) :
    a - b = a - c ↔ b = c :=
  (cancel_of_ne ha).tsub_right_inj (cancel_of_ne <| ne_top_of_le_ne_top ha hb)
    (cancel_of_ne <| ne_top_of_le_ne_top ha hc) hb hc
Right Subtraction Cancellation in Extended Non-Negative Reals: $a - b = a - c \leftrightarrow b = c$
Informal description
For any extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a \neq \infty$ and $b, c \leq a$, then the equality $a - b = a - c$ holds if and only if $b = c$.
ENNReal.sub_mul theorem
(h : 0 < b → b < a → c ≠ ∞) : (a - b) * c = a * c - b * c
Full source 
protected theorem sub_mul (h : 0 < b → b < a → c ≠ ∞) : (a - b) * c = a * c - b * c := by
  rcases le_or_lt a b with hab | hab; · simp [hab, mul_right_mono hab, tsub_eq_zero_of_le]
  rcases eq_or_lt_of_le (zero_le b) with (rfl | hb); · simp
  exact (cancel_of_ne <| mul_ne_top hab.ne_top (h hb hab)).tsub_mul
Distributivity of Subtraction over Multiplication in Extended Non-Negative Reals
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $0 < b < a$ implies $c \neq \infty$, then $(a - b) \cdot c = a \cdot c - b \cdot c$.
ENNReal.mul_sub theorem
(h : 0 < c → c < b → a ≠ ∞) : a * (b - c) = a * b - a * c
Full source 
protected theorem mul_sub (h : 0 < c → c < b → a ≠ ∞) : a * (b - c) = a * b - a * c := by
  simp only [mul_comm a]
  exact ENNReal.sub_mul h
Distributivity of Multiplication over Subtraction in Extended Non-Negative Reals: $a \cdot (b - c) = a \cdot b - a \cdot c$ when $a \neq \infty$ for $0 < c < b$
Informal description
For extended non-negative real numbers $a, b, c \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $0 < c < b$ implies $a \neq \infty$, then $a \cdot (b - c) = a \cdot b - a \cdot c$.
ENNReal.sub_le_sub_iff_left theorem
(h : c ≤ a) (h' : a ≠ ∞) : (a - b ≤ a - c) ↔ c ≤ b
Full source 
theorem sub_le_sub_iff_left (h : c ≤ a) (h' : a ≠ ∞) :
    (a - b ≤ a - c) ↔ c ≤ b :=
  (cancel_of_ne h').tsub_le_tsub_iff_left (cancel_of_ne (ne_top_of_le_ne_top h' h)) h
Subtraction Order Reversal in Extended Non-Negative Reals: $a - b \leq a - c \leftrightarrow c \leq b$ when $c \leq a$ and $a \neq \infty$
Informal description
For extended non-negative real numbers $a, b, c$ with $c \leq a$ and $a \neq \infty$, the inequality $a - b \leq a - c$ holds if and only if $c \leq b$.
ENNReal.le_toReal_sub theorem
{a b : ℝ≥0∞} (hb : b ≠ ∞) : a.toReal - b.toReal ≤ (a - b).toReal
Full source 
theorem le_toReal_sub {a b : ℝ≥0∞} (hb : b ≠ ∞) : a.toReal - b.toReal ≤ (a - b).toReal := by
  lift b to ℝ≥0 using hb
  induction a
  · simp
  · simp only [← coe_sub, NNReal.sub_def, Real.coe_toNNReal', coe_toReal]
    exact le_max_left _ _
Inequality for Real Projection of Subtraction in Extended Non-Negative Reals: $a_\mathbb{R} - b_\mathbb{R} \leq (a - b)_\mathbb{R}$ when $b \neq \infty$
Informal description
For any extended non-negative real numbers $a$ and $b$ with $b \neq \infty$, the difference of their real projections satisfies $a.\text{toReal} - b.\text{toReal} \leq (a - b).\text{toReal}$.
ENNReal.toNNReal_sub theorem
(hb : b ≠ ∞) : (a - b).toNNReal = a.toNNReal - b.toNNReal
Full source 
@[simp]
lemma toNNReal_sub (hb : b ≠ ∞) : (a - b).toNNReal = a.toNNReal - b.toNNReal := by
  lift b to ℝ≥0 using hb; induction a <;> simp [← coe_sub]
Non-Negative Real Projection of Subtraction in Extended Non-Negative Reals: $(a - b)_{\text{NN}} = a_{\text{NN}} - b_{\text{NN}}$ when $b \neq \infty$
Informal description
For any extended non-negative real numbers $a$ and $b$ with $b \neq \infty$, the non-negative real projection of their difference equals the difference of their non-negative real projections, i.e., $(a - b).\text{toNNReal} = a.\text{toNNReal} - b.\text{toNNReal}$.
ENNReal.toReal_sub_of_le theorem
(hba : b ≤ a) (ha : a ≠ ∞) : (a - b).toReal = a.toReal - b.toReal
Full source 
@[simp]
lemma toReal_sub_of_le (hba : b ≤ a) (ha : a ≠ ∞) : (a - b).toReal = a.toReal - b.toReal := by
  simp [ENNReal.toReal, ne_top_of_le_ne_top ha hba, toNNReal_mono ha hba]
Real Projection of Subtraction in Extended Non-Negative Reals Under Order Condition: $(a - b)_\mathbb{R} = a_\mathbb{R} - b_\mathbb{R}$ when $b \leq a$ and $a \neq \infty$
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $b \leq a$ and $a \neq \infty$, the real projection of their difference equals the difference of their real projections, i.e., $(a - b).\text{toReal} = a.\text{toReal} - b.\text{toReal}$.
ENNReal.ofReal_sub theorem
(p : ℝ) {q : ℝ} (hq : 0 ≤ q) : ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q
Full source 
theorem ofReal_sub (p : ℝ) {q : ℝ} (hq : 0 ≤ q) :
    ENNReal.ofReal (p - q) = ENNReal.ofReal p - ENNReal.ofReal q := by
  obtain h | h := le_total p q
  · rw [ofReal_of_nonpos (sub_nonpos_of_le h), tsub_eq_zero_of_le (ofReal_le_ofReal h)]
  refine ENNReal.eq_sub_of_add_eq ofReal_ne_top ?_
  rw [← ofReal_add (sub_nonneg_of_le h) hq, sub_add_cancel]
Subtractivity of `ofReal` for Nonnegative Reals
Informal description
For any real number $p$ and any nonnegative real number $q$ (i.e., $q \geq 0$), the extended nonnegative real number obtained by applying the `ofReal` function to their difference $p - q$ is equal to the difference of the `ofReal` function applied to each number individually. In other words, $\text{ofReal}(p - q) = \text{ofReal}(p) - \text{ofReal}(q)$.
ENNReal.Ico_eq_Iio theorem
: Ico 0 y = Iio y
Full source 
protected theorem Ico_eq_Iio : Ico 0 y = Iio y :=
  Ico_bot
Equality of Zero-Based Interval and Strictly Below Interval in Extended Non-Negative Reals: $[0, y) = (-\infty, y)$
Informal description
For any extended non-negative real number $y$, the left-closed right-open interval $[0, y)$ is equal to the left-infinite right-open interval $(-\infty, y)$.
ENNReal.mem_Iio_self_add theorem
: x ≠ ∞ → ε ≠ 0 → x ∈ Iio (x + ε)
Full source 
theorem mem_Iio_self_add : x ≠ ∞ → ε ≠ 0 → x ∈ Iio (x + ε) := fun xt ε0 => lt_add_right xt ε0
Self-addition preserves membership in left-infinite interval for extended non-negative reals
Informal description
For any finite extended non-negative real number $x$ (i.e., $x \neq \infty$) and any non-zero extended non-negative real number $\varepsilon$ (i.e., $\varepsilon \neq 0$), the element $x$ belongs to the left-infinite right-open interval $(-\infty, x + \varepsilon)$.
ENNReal.mem_Ioo_self_sub_add theorem
: x ≠ ∞ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 0 → x ∈ Ioo (x - ε₁) (x + ε₂)
Full source 
theorem mem_Ioo_self_sub_add : x ≠ ∞ → x ≠ 0 → ε₁ ≠ 0 → ε₂ ≠ 0 → x ∈ Ioo (x - ε₁) (x + ε₂) :=
  fun xt x0 ε0 ε0' => ⟨ENNReal.sub_lt_self xt x0 ε0, lt_add_right xt ε0'⟩
Membership in Open Interval Around Self via Truncated Subtraction and Addition in Extended Non-Negative Reals
Informal description
For any extended non-negative real number $x$ such that $x$ is finite and nonzero ($x \neq \infty$ and $x \neq 0$), and for any nonzero extended non-negative real numbers $\varepsilon_1$ and $\varepsilon_2$ ($\varepsilon_1 \neq 0$ and $\varepsilon_2 \neq 0$), the element $x$ belongs to the open interval $(x - \varepsilon_1, x + \varepsilon_2)$.
ENNReal.image_coe_Iic theorem
(x : ℝ≥0) : (↑) '' Iic x = Iic (x : ℝ≥0∞)
Full source 
@[simp]
theorem image_coe_Iic (x : ℝ≥0) : (↑)(↑) '' Iic x = Iic (x : ℝ≥0∞) := WithTop.image_coe_Iic
Image of Closed Interval under Extended Nonnegative Real Embedding
Informal description
For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the image of the closed interval $(-\infty, x]$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the closed interval $(-\infty, x]$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_Ici theorem
(x : ℝ≥0) : (↑) '' Ici x = Ico ↑x ∞
Full source 
@[simp]
theorem image_coe_Ici (x : ℝ≥0) : (↑)(↑) '' Ici x = Ico ↑x ∞ := WithTop.image_coe_Ici
Image of $[x, \infty)$ under embedding equals $[x, \infty)$ in extended nonnegative reals
Informal description
For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the image of the closed interval $[x, \infty)$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the left-closed right-open interval $[x, \infty)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_Iio theorem
(x : ℝ≥0) : (↑) '' Iio x = Iio (x : ℝ≥0∞)
Full source 
@[simp]
theorem image_coe_Iio (x : ℝ≥0) : (↑)(↑) '' Iio x = Iio (x : ℝ≥0∞) := WithTop.image_coe_Iio
Image of Open Interval under Embedding into Extended Nonnegative Reals
Informal description
For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the image of the open interval $(-\infty, x)$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the open interval $(-\infty, x)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_Ioi theorem
(x : ℝ≥0) : (↑) '' Ioi x = Ioo ↑x ∞
Full source 
@[simp]
theorem image_coe_Ioi (x : ℝ≥0) : (↑)(↑) '' Ioi x = Ioo ↑x ∞ := WithTop.image_coe_Ioi
Image of Right-Infinite Interval under Embedding Equals Open Interval in Extended Nonnegative Reals
Informal description
For any nonnegative real number $x \in \mathbb{R}_{\geq 0}$, the image of the right-infinite open interval $(x, \infty)$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the open interval $(x, \infty)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_Icc theorem
(x y : ℝ≥0) : (↑) '' Icc x y = Icc (x : ℝ≥0∞) y
Full source 
@[simp]
theorem image_coe_Icc (x y : ℝ≥0) : (↑)(↑) '' Icc x y = Icc (x : ℝ≥0∞) y := WithTop.image_coe_Icc
Image of Closed Interval under Embedding into Extended Nonnegative Reals
Informal description
For any nonnegative real numbers $x$ and $y$ in $\mathbb{R}_{\geq 0}$, the image of the closed interval $[x, y]$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the closed interval $[x, y]$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_Ico theorem
(x y : ℝ≥0) : (↑) '' Ico x y = Ico (x : ℝ≥0∞) y
Full source 
@[simp]
theorem image_coe_Ico (x y : ℝ≥0) : (↑)(↑) '' Ico x y = Ico (x : ℝ≥0∞) y := WithTop.image_coe_Ico
Image of $[x, y)$ under embedding equals $[x, y)$ in extended nonnegative reals
Informal description
For any nonnegative real numbers $x$ and $y$ in $\mathbb{R}_{\geq 0}$, the image of the left-closed right-open interval $[x, y)$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the left-closed right-open interval $[x, y)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_Ioc theorem
(x y : ℝ≥0) : (↑) '' Ioc x y = Ioc (x : ℝ≥0∞) y
Full source 
@[simp]
theorem image_coe_Ioc (x y : ℝ≥0) : (↑)(↑) '' Ioc x y = Ioc (x : ℝ≥0∞) y := WithTop.image_coe_Ioc
Image of $(x, y]$ under canonical embedding to extended nonnegative reals
Informal description
For any nonnegative real numbers $x$ and $y$ in $\mathbb{R}_{\geq 0}$, the image of the left-open right-closed interval $(x, y]$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the left-open right-closed interval $(x, y]$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_Ioo theorem
(x y : ℝ≥0) : (↑) '' Ioo x y = Ioo (x : ℝ≥0∞) y
Full source 
@[simp]
theorem image_coe_Ioo (x y : ℝ≥0) : (↑)(↑) '' Ioo x y = Ioo (x : ℝ≥0∞) y := WithTop.image_coe_Ioo
Image of Open Interval under Canonical Embedding in Extended Nonnegative Reals
Informal description
For any nonnegative real numbers $x$ and $y$ in $\mathbb{R}_{\geq 0}$, the image of the open interval $(x, y)$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the open interval $(x, y)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_uIcc theorem
(x y : ℝ≥0) : (↑) '' uIcc x y = uIcc (x : ℝ≥0∞) y
Full source 
@[simp]
theorem image_coe_uIcc (x y : ℝ≥0) : (↑)(↑) '' uIcc x y = uIcc (x : ℝ≥0∞) y := by simp [uIcc]
Image of Unordered Closed Interval under Embedding into Extended Nonnegative Reals
Informal description
For any nonnegative real numbers $x$ and $y$ in $\mathbb{R}_{\geq 0}$, the image of the unordered closed interval $[x \sqcap y, x \sqcup y]$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the unordered closed interval $[x \sqcap y, x \sqcup y]$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_uIoc theorem
(x y : ℝ≥0) : (↑) '' uIoc x y = uIoc (x : ℝ≥0∞) y
Full source 
@[simp]
theorem image_coe_uIoc (x y : ℝ≥0) : (↑)(↑) '' uIoc x y = uIoc (x : ℝ≥0∞) y := by simp [uIoc]
Image of Open-Closed Interval under Canonical Embedding to Extended Nonnegative Reals
Informal description
For any nonnegative real numbers $x$ and $y$ in $\mathbb{R}_{\geq 0}$, the image of the open-closed interval $\text{uIoc}(x, y) = \{z \in \mathbb{R}_{\geq 0} \mid \min(x, y) < z \leq \max(x, y)\}$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the open-closed interval $\text{uIoc}(x, y)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
ENNReal.image_coe_uIoo theorem
(x y : ℝ≥0) : (↑) '' uIoo x y = uIoo (x : ℝ≥0∞) y
Full source 
@[simp]
theorem image_coe_uIoo (x y : ℝ≥0) : (↑)(↑) '' uIoo x y = uIoo (x : ℝ≥0∞) y := by simp [uIoo]
Image of Open Unordered Interval under Embedding into Extended Nonnegative Reals
Informal description
For any nonnegative real numbers $x$ and $y$ in $\mathbb{R}_{\geq 0}$, the image of the open unordered interval $\text{uIoo}(x, y) = \{z \in \mathbb{R}_{\geq 0} \mid \min(x, y) < z < \max(x, y)\}$ under the canonical embedding $\mathbb{R}_{\geq 0} \hookrightarrow \mathbb{R}_{\geq 0} \cup \{\infty\}$ is equal to the open unordered interval $\text{uIoo}(x, y)$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.