doc-next-gen

Mathlib.Data.ENNReal.Real

Module docstring

{"# Maps between real and extended non-negative real numbers

This file focuses on the functions ENNReal.toReal : ℝ≥0∞ → ℝ and ENNReal.ofReal : ℝ → ℝ≥0∞ which were defined in Data.ENNReal.Basic. It collects all the basic results of the interactions between these functions and the algebraic and lattice operations, although a few may appear in earlier files.

This file provides a positivity extension for ENNReal.ofReal.

Main theorems

  • trichotomy (p : ℝ≥0∞) : p = 0 ∨ p = ∞ ∨ 0 < p.toReal: often used for WithLp and lp
  • dichotomy (p : ℝ≥0∞) [Fact (1 ≤ p)] : p = ∞ ∨ 1 ≤ p.toReal: often used for WithLp and lp
  • toNNReal_iInf through toReal_sSup: these declarations allow for easy conversions between indexed or set infima and suprema in ℝ, ℝ≥0 and ℝ≥0∞. This is especially useful because ℝ≥0∞ is a complete lattice. "}
ENNReal.toReal_add theorem
(ha : a ≠ ∞) (hb : b ≠ ∞) : (a + b).toReal = a.toReal + b.toReal
Full source 
theorem toReal_add (ha : a ≠ ∞) (hb : b ≠ ∞) : (a + b).toReal = a.toReal + b.toReal := by
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  rfl
Additivity of `toReal` for Finite Extended Nonnegative Reals
Informal description
For any extended nonnegative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, the real number obtained by applying the `toReal` function to their sum is equal to the sum of the `toReal` function applied to each number individually. In other words, $(a + b).\text{toReal} = a.\text{toReal} + b.\text{toReal}$.
ENNReal.toReal_add_le theorem
: (a + b).toReal ≤ a.toReal + b.toReal
Full source 
theorem toReal_add_le : (a + b).toReal ≤ a.toReal + b.toReal :=
  if ha : a = ∞ then by simp only [ha, top_add, toReal_top, zero_add, toReal_nonneg]
  else
    if hb : b = ∞ then by simp only [hb, add_top, toReal_top, add_zero, toReal_nonneg]
    else le_of_eq (toReal_add ha hb)
Subadditivity of `toReal` for Extended Nonnegative Reals
Informal description
For any extended nonnegative real numbers $a$ and $b$, the real number obtained by applying the `toReal` function to their sum is less than or equal to the sum of the `toReal` function applied to each number individually. In other words, $(a + b).\text{toReal} \leq a.\text{toReal} + b.\text{toReal}$.
ENNReal.ofReal_add theorem
{p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) : ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q
Full source 
theorem ofReal_add {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :
    ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q := by
  rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj,
    Real.toNNReal_add hp hq]
Additivity of `ofReal` for Nonnegative Reals
Informal description
For any nonnegative real numbers $p$ and $q$ (i.e., $p \geq 0$ and $q \geq 0$), the extended nonnegative real number obtained by applying the `ofReal` function to their sum is equal to the sum of the `ofReal` function applied to each number individually. In other words, $\text{ofReal}(p + q) = \text{ofReal}(p) + \text{ofReal}(q)$.
ENNReal.ofReal_add_le theorem
{p q : ℝ} : ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q
Full source 
theorem ofReal_add_le {p q : ℝ} : ENNReal.ofReal (p + q) ≤ ENNReal.ofReal p + ENNReal.ofReal q :=
  coe_le_coe.2 Real.toNNReal_add_le
Subadditivity of `ENNReal.ofReal`
Informal description
For any real numbers $p$ and $q$, the extended non-negative real number obtained by applying `ENNReal.ofReal` to their sum is less than or equal to the sum of the extended non-negative real numbers obtained by applying `ENNReal.ofReal` to $p$ and $q$ individually. In other words, \[ \text{ENNReal.ofReal}(p + q) \leq \text{ENNReal.ofReal}(p) + \text{ENNReal.ofReal}(q). \]
ENNReal.toReal_le_toReal theorem
(ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal ≤ b.toReal ↔ a ≤ b
Full source 
@[simp]
theorem toReal_le_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal ≤ b.toReal ↔ a ≤ b := by
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  norm_cast
Inequality Preservation Between Extended and Standard Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, the inequality $a \leq b$ holds if and only if their real-valued counterparts satisfy $a.\text{toReal} \leq b.\text{toReal}$.
ENNReal.toReal_mono theorem
(hb : b ≠ ∞) (h : a ≤ b) : a.toReal ≤ b.toReal
Full source 
@[gcongr]
theorem toReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toReal ≤ b.toReal :=
  (toReal_le_toReal (ne_top_of_le_ne_top hb h) hb).2 h
Monotonicity of Real Projection for Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $b \neq \infty$, if $a \leq b$, then the real-valued projection of $a$ is less than or equal to the real-valued projection of $b$, i.e., $a.\text{toReal} \leq b.\text{toReal}$.
ENNReal.toReal_mono' theorem
(h : a ≤ b) (ht : b = ∞ → a = ∞) : a.toReal ≤ b.toReal
Full source 
theorem toReal_mono' (h : a ≤ b) (ht : b = ∞ → a = ∞) : a.toReal ≤ b.toReal := by
  rcases eq_or_ne a ∞ with rfl | ha
  · exact toReal_nonneg
  · exact toReal_mono (mt ht ha) h
Monotonicity of Real Projection for Extended Non-Negative Reals with Infinity Condition
Informal description
For any extended non-negative real numbers $a$ and $b$ such that if $b = \infty$ then $a = \infty$, if $a \leq b$, then the real-valued projection of $a$ is less than or equal to the real-valued projection of $b$, i.e., $\text{toReal}(a) \leq \text{toReal}(b)$.
ENNReal.toReal_lt_toReal theorem
(ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal < b.toReal ↔ a < b
Full source 
@[simp]
theorem toReal_lt_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal < b.toReal ↔ a < b := by
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  norm_cast
Comparison of Extended Non-Negative Reals via Their Real Projections
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, the inequality $a < b$ holds if and only if their real counterparts satisfy $a.\text{toReal} < b.\text{toReal}$.
ENNReal.toReal_strict_mono theorem
(hb : b ≠ ∞) (h : a < b) : a.toReal < b.toReal
Full source 
@[gcongr]
theorem toReal_strict_mono (hb : b ≠ ∞) (h : a < b) : a.toReal < b.toReal :=
  (toReal_lt_toReal h.ne_top hb).2 h
Strict Monotonicity of Real Projection for Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $b \neq \infty$, if $a < b$, then the real projection of $a$ is strictly less than the real projection of $b$, i.e., $a.\text{toReal} < b.\text{toReal}$.
ENNReal.toNNReal_mono theorem
(hb : b ≠ ∞) (h : a ≤ b) : a.toNNReal ≤ b.toNNReal
Full source 
@[gcongr]
theorem toNNReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toNNReal ≤ b.toNNReal :=
  toReal_mono hb h
Monotonicity of Non-Negative Real Projection for Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $b \neq \infty$, if $a \leq b$, then the non-negative real projection of $a$ is less than or equal to the non-negative real projection of $b$, i.e., $a.\text{toNNReal} \leq b.\text{toNNReal}$.
ENNReal.le_toNNReal_of_coe_le theorem
(h : p ≤ a) (ha : a ≠ ∞) : p ≤ a.toNNReal
Full source 
theorem le_toNNReal_of_coe_le (h : p ≤ a) (ha : a ≠ ∞) : p ≤ a.toNNReal :=
  @toNNReal_coe p ▸ toNNReal_mono ha h
Inequality Preservation under Projection to Non-Negative Reals
Informal description
For any extended non-negative real numbers $p$ and $a$ such that $a \neq \infty$, if $p \leq a$, then $p \leq a.\text{toNNReal}$.
ENNReal.toNNReal_le_toNNReal theorem
(ha : a ≠ ∞) (hb : b ≠ ∞) : a.toNNReal ≤ b.toNNReal ↔ a ≤ b
Full source 
@[simp]
theorem toNNReal_le_toNNReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toNNReal ≤ b.toNNReal ↔ a ≤ b :=
  ⟨fun h => by rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_le_coe], toNNReal_mono hb⟩
Inequality Equivalence between Extended Non-Negative Reals and Their Non-Negative Real Projections
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, the inequality $a_{\text{toNNReal}} \leq b_{\text{toNNReal}}$ holds if and only if $a \leq b$.
ENNReal.toNNReal_strict_mono theorem
(hb : b ≠ ∞) (h : a < b) : a.toNNReal < b.toNNReal
Full source 
@[gcongr]
theorem toNNReal_strict_mono (hb : b ≠ ∞) (h : a < b) : a.toNNReal < b.toNNReal := by
  simpa [← ENNReal.coe_lt_coe, hb, h.ne_top]
Strict Monotonicity of the Non-Negative Real Part for Extended Non-Negative Real Numbers
Informal description
For any extended non-negative real numbers $a$ and $b$ with $b \neq \infty$, if $a < b$, then the non-negative real part of $a$ is strictly less than the non-negative real part of $b$, i.e., $a_{\text{toNNReal}} < b_{\text{toNNReal}}$.
ENNReal.toNNReal_lt_toNNReal theorem
(ha : a ≠ ∞) (hb : b ≠ ∞) : a.toNNReal < b.toNNReal ↔ a < b
Full source 
@[simp]
theorem toNNReal_lt_toNNReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toNNReal < b.toNNReal ↔ a < b :=
  ⟨fun h => by rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe], toNNReal_strict_mono hb⟩
Inequality Preservation between Extended Non-Negative Reals and Their Non-Negative Real Parts
Informal description
For any extended non-negative real numbers $a$ and $b$ with $a \neq \infty$ and $b \neq \infty$, the inequality $a_{\text{toNNReal}} < b_{\text{toNNReal}}$ holds if and only if $a < b$.
ENNReal.toNNReal_lt_of_lt_coe theorem
(h : a < p) : a.toNNReal < p
Full source 
theorem toNNReal_lt_of_lt_coe (h : a < p) : a.toNNReal < p :=
  @toNNReal_coe p ▸ toNNReal_strict_mono coe_ne_top h
Non-Negative Real Part Bound from Extended Non-Negative Real Inequality
Informal description
For any extended non-negative real number $a$ and any non-negative real number $p$, if $a < p$, then the non-negative real part of $a$ is strictly less than $p$, i.e., $a_{\text{toNNReal}} < p$.
ENNReal.toReal_max theorem
(hr : a ≠ ∞) (hp : b ≠ ∞) : ENNReal.toReal (max a b) = max (ENNReal.toReal a) (ENNReal.toReal b)
Full source 
theorem toReal_max (hr : a ≠ ∞) (hp : b ≠ ∞) :
    ENNReal.toReal (max a b) = max (ENNReal.toReal a) (ENNReal.toReal b) :=
  (le_total a b).elim
    (fun h => by simp only [h, ENNReal.toReal_mono hp h, max_eq_right]) fun h => by
    simp only [h, ENNReal.toReal_mono hr h, max_eq_left]
Maximum Preservation under Real Projection for Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, the real-valued projection of the maximum of $a$ and $b$ is equal to the maximum of their real-valued projections, i.e., $\text{toReal}(\max(a, b)) = \max(\text{toReal}(a), \text{toReal}(b))$.
ENNReal.toReal_min theorem
{a b : ℝ≥0∞} (hr : a ≠ ∞) (hp : b ≠ ∞) : ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b)
Full source 
theorem toReal_min {a b : ℝ≥0∞} (hr : a ≠ ∞) (hp : b ≠ ∞) :
    ENNReal.toReal (min a b) = min (ENNReal.toReal a) (ENNReal.toReal b) :=
  (le_total a b).elim (fun h => by simp only [h, ENNReal.toReal_mono hp h, min_eq_left])
    fun h => by simp only [h, ENNReal.toReal_mono hr h, min_eq_right]
Minimum Preservation under Real Projection for Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, the real-valued projection of the minimum of $a$ and $b$ is equal to the minimum of their real-valued projections, i.e., $\text{toReal}(\min(a, b)) = \min(\text{toReal}(a), \text{toReal}(b))$.
ENNReal.toReal_sup theorem
{a b : ℝ≥0∞} : a ≠ ∞ → b ≠ ∞ → (a ⊔ b).toReal = a.toReal ⊔ b.toReal
Full source 
theorem toReal_sup {a b : ℝ≥0∞} : a ≠ ∞ → b ≠ ∞ → (a ⊔ b).toReal = a.toReal ⊔ b.toReal :=
  toReal_max
Supremum Preservation under Real Projection for Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, the real-valued projection of the supremum of $a$ and $b$ is equal to the supremum of their real-valued projections, i.e., $\text{toReal}(a \sqcup b) = \text{toReal}(a) \sqcup \text{toReal}(b)$.
ENNReal.toReal_inf theorem
{a b : ℝ≥0∞} : a ≠ ∞ → b ≠ ∞ → (a ⊓ b).toReal = a.toReal ⊓ b.toReal
Full source 
theorem toReal_inf {a b : ℝ≥0∞} : a ≠ ∞ → b ≠ ∞ → (a ⊓ b).toReal = a.toReal ⊓ b.toReal :=
  toReal_min
Infimum Preservation under Real Projection for Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, the real-valued projection of the infimum of $a$ and $b$ is equal to the infimum of their real-valued projections, i.e., $\text{toReal}(a \sqcap b) = \text{toReal}(a) \sqcap \text{toReal}(b)$.
ENNReal.toNNReal_pos_iff theorem
: 0 < a.toNNReal ↔ 0 < a ∧ a < ∞
Full source 
theorem toNNReal_pos_iff : 0 < a.toNNReal ↔ 0 < a ∧ a < ∞ := by
  induction a <;> simp
Positivity of Extended Non-Negative Real's Finite Part: $0 < a_{\text{NN}} \leftrightarrow (0 < a \land a < \infty)$
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the canonical non-negative real part $a_{\text{NN}}$ (obtained by dropping the $\infty$ case) satisfies $0 < a_{\text{NN}}$ if and only if $0 < a$ and $a < \infty$.
ENNReal.toNNReal_pos theorem
{a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ∞) : 0 < a.toNNReal
Full source 
theorem toNNReal_pos {a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ∞) : 0 < a.toNNReal :=
  toNNReal_pos_iff.mpr ⟨bot_lt_iff_ne_bot.mpr ha₀, lt_top_iff_ne_top.mpr ha_top⟩
Positivity of Extended Non-Negative Real's Finite Part under Non-Zero and Finite Conditions
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a$ is neither zero nor infinity, then the canonical non-negative real part $a_{\text{NN}}$ (obtained by dropping the $\infty$ case) is strictly positive, i.e., $0 < a_{\text{NN}}$.
ENNReal.toReal_pos_iff theorem
: 0 < a.toReal ↔ 0 < a ∧ a < ∞
Full source 
theorem toReal_pos_iff : 0 < a.toReal ↔ 0 < a ∧ a < ∞ :=
  NNReal.coe_pos.trans toNNReal_pos_iff
Positivity of Extended Non-Negative Real's Real Part: $0 < a_{\text{real}} \leftrightarrow (0 < a \land a < \infty)$
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the real part $a_{\text{real}}$ (obtained by mapping $\infty$ to $0$) satisfies $0 < a_{\text{real}}$ if and only if $0 < a$ and $a < \infty$.
ENNReal.toReal_pos theorem
{a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ∞) : 0 < a.toReal
Full source 
theorem toReal_pos {a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ∞) : 0 < a.toReal :=
  toReal_pos_iff.mpr ⟨bot_lt_iff_ne_bot.mpr ha₀, lt_top_iff_ne_top.mpr ha_top⟩
Positivity of Extended Non-Negative Real's Real Part under Non-Zero and Finite Conditions
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $a$ is neither zero nor infinity, then its real part $a_{\text{real}}$ is strictly positive, i.e., $0 < a_{\text{real}}$.
ENNReal.ofReal_le_ofReal theorem
{p q : ℝ} (h : p ≤ q) : ENNReal.ofReal p ≤ ENNReal.ofReal q
Full source 
@[gcongr, bound]
theorem ofReal_le_ofReal {p q : ℝ} (h : p ≤ q) : ENNReal.ofReal p ≤ ENNReal.ofReal q := by
  simp [ENNReal.ofReal, Real.toNNReal_le_toNNReal h]
Monotonicity of Extended Non-Negative Real Conversion
Informal description
For any real numbers $p$ and $q$ such that $p \leq q$, the extended non-negative real number obtained by applying the `ENNReal.ofReal` function to $p$ is less than or equal to the extended non-negative real number obtained by applying the same function to $q$, i.e., $\text{ENNReal.ofReal}(p) \leq \text{ENNReal.ofReal}(q)$.
ENNReal.ofReal_le_of_le_toReal theorem
{a : ℝ} {b : ℝ≥0∞} (h : a ≤ ENNReal.toReal b) : ENNReal.ofReal a ≤ b
Full source 
theorem ofReal_le_of_le_toReal {a : ℝ} {b : ℝ≥0∞} (h : a ≤ ENNReal.toReal b) :
    ENNReal.ofReal a ≤ b :=
  (ofReal_le_ofReal h).trans ofReal_toReal_le
Comparison between Real and Extended Non-Negative Reals via `ofReal` and `toReal`
Informal description
For any real number $a$ and extended non-negative real number $b$, if $a \leq \text{ENNReal.toReal}(b)$, then $\text{ENNReal.ofReal}(a) \leq b$.
ENNReal.ofReal_le_ofReal_iff theorem
{p q : ℝ} (h : 0 ≤ q) : ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q
Full source 
@[simp]
theorem ofReal_le_ofReal_iff {p q : ℝ} (h : 0 ≤ q) :
    ENNReal.ofRealENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q := by
  rw [ENNReal.ofReal, ENNReal.ofReal, coe_le_coe, Real.toNNReal_le_toNNReal_iff h]
Inequality Preservation of Extended Non-Negative Real Conversion
Informal description
For any real numbers $p$ and $q$ with $q \geq 0$, the inequality $\text{ENNReal.ofReal}(p) \leq \text{ENNReal.ofReal}(q)$ holds if and only if $p \leq q$.
ENNReal.ofReal_le_ofReal_iff' theorem
{p q : ℝ} : ENNReal.ofReal p ≤ .ofReal q ↔ p ≤ q ∨ p ≤ 0
Full source 
lemma ofReal_le_ofReal_iff' {p q : ℝ} : ENNReal.ofRealENNReal.ofReal p ≤ .ofReal q ↔ p ≤ q ∨ p ≤ 0 :=
  coe_le_coe.trans Real.toNNReal_le_toNNReal_iff'
Comparison of Extended Non-Negative Reals via `ofReal`: $p \leq q$ or $p \leq 0$
Informal description
For any real numbers $p$ and $q$, the extended non-negative real number obtained by applying `ENNReal.ofReal` to $p$ is less than or equal to that obtained from $q$ if and only if either $p \leq q$ or $p \leq 0$.
ENNReal.ofReal_lt_ofReal_iff' theorem
{p q : ℝ} : ENNReal.ofReal p < .ofReal q ↔ p < q ∧ 0 < q
Full source 
lemma ofReal_lt_ofReal_iff' {p q : ℝ} : ENNReal.ofRealENNReal.ofReal p < .ofReal q ↔ p < q ∧ 0 < q :=
  coe_lt_coe.trans Real.toNNReal_lt_toNNReal_iff'
Strict Inequality for Extended Non-Negative Reals via `ofReal`: $p < q \land 0 < q \leftrightarrow \text{ofReal}(p) < \text{ofReal}(q)$
Informal description
For any real numbers $p$ and $q$, the extended non-negative real number obtained by applying the `ofReal` function to $p$ is strictly less than that obtained from $q$ if and only if $p < q$ and $0 < q$.
ENNReal.ofReal_eq_ofReal_iff theorem
{p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) : ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q
Full source 
@[simp]
theorem ofReal_eq_ofReal_iff {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :
    ENNReal.ofRealENNReal.ofReal p = ENNReal.ofReal q ↔ p = q := by
  rw [ENNReal.ofReal, ENNReal.ofReal, coe_inj, Real.toNNReal_eq_toNNReal_iff hp hq]
Equality of Extended Non-Negative Reals from Non-Negative Reals
Informal description
For any nonnegative real numbers $p$ and $q$ (i.e., $p \geq 0$ and $q \geq 0$), the extended non-negative real numbers obtained by applying the `ENNReal.ofReal` function to $p$ and $q$ are equal if and only if $p = q$. In other words, $\text{ENNReal.ofReal}(p) = \text{ENNReal.ofReal}(q) \leftrightarrow p = q$.
ENNReal.ofReal_lt_ofReal_iff theorem
{p q : ℝ} (h : 0 < q) : ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
Full source 
@[simp]
theorem ofReal_lt_ofReal_iff {p q : ℝ} (h : 0 < q) :
    ENNReal.ofRealENNReal.ofReal p < ENNReal.ofReal q ↔ p < q := by
  rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]
Comparison of Extended Non-Negative Reals via $\text{ofReal}$ under Positive Condition
Informal description
For real numbers $p$ and $q$ with $0 < q$, the extended non-negative real number $\text{ofReal}(p)$ is less than $\text{ofReal}(q)$ if and only if $p < q$.
ENNReal.ofReal_lt_ofReal_iff_of_nonneg theorem
{p q : ℝ} (hp : 0 ≤ p) : ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
Full source 
theorem ofReal_lt_ofReal_iff_of_nonneg {p q : ℝ} (hp : 0 ≤ p) :
    ENNReal.ofRealENNReal.ofReal p < ENNReal.ofReal q ↔ p < q := by
  rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]
Strict Inequality Preservation for Nonnegative Reals under `ofReal` Embedding
Informal description
For any nonnegative real numbers $p$ and $q$ (with $p \geq 0$), the extended non-negative real number obtained by applying the `ofReal` function to $p$ is less than that obtained from $q$ if and only if $p < q$. In other words, $[p] < [q] \leftrightarrow p < q$, where $[ \cdot ]$ denotes the `ofReal` embedding.
ENNReal.ofReal_pos theorem
{p : ℝ} : 0 < ENNReal.ofReal p ↔ 0 < p
Full source 
@[simp]
theorem ofReal_pos {p : ℝ} : 0 < ENNReal.ofReal p ↔ 0 < p := by simp [ENNReal.ofReal]
Positivity of Extended Non-Negative Real Numbers via $\text{ofReal}$
Informal description
For any real number $p$, the extended non-negative real number $\text{ofReal}(p)$ is strictly positive if and only if $p$ is strictly positive, i.e., $0 < \text{ofReal}(p) \leftrightarrow 0 < p$.
ENNReal.ofReal_eq_zero theorem
{p : ℝ} : ENNReal.ofReal p = 0 ↔ p ≤ 0
Full source 
@[simp]
theorem ofReal_eq_zero {p : ℝ} : ENNReal.ofRealENNReal.ofReal p = 0 ↔ p ≤ 0 := by simp [ENNReal.ofReal]
Characterization of Zero in Extended Non-Negative Reals: $\text{ofReal}(p) = 0 \leftrightarrow p \leq 0$
Informal description
For any real number $p$, the extended non-negative real number obtained by applying the function $\text{ofReal}(p)$ equals zero if and only if $p \leq 0$.
ENNReal.ofReal_ne_zero_iff theorem
{r : ℝ} : ENNReal.ofReal r ≠ 0 ↔ 0 < r
Full source 
theorem ofReal_ne_zero_iff {r : ℝ} : ENNReal.ofRealENNReal.ofReal r ≠ 0ENNReal.ofReal r ≠ 0 ↔ 0 < r := by
  rw [← zero_lt_iff, ENNReal.ofReal_pos]
Nonzero Criterion for Extended Non-Negative Reals: $\text{ofReal}(r) \neq 0 \leftrightarrow r > 0$
Informal description
For any real number $r$, the extended non-negative real number $\text{ENNReal.ofReal}(r)$ is nonzero if and only if $r$ is strictly positive, i.e., $\text{ENNReal.ofReal}(r) \neq 0 \leftrightarrow 0 < r$.
ENNReal.zero_eq_ofReal theorem
{p : ℝ} : 0 = ENNReal.ofReal p ↔ p ≤ 0
Full source 
@[simp]
theorem zero_eq_ofReal {p : ℝ} : 0 = ENNReal.ofReal p ↔ p ≤ 0 :=
  eq_comm.trans ofReal_eq_zero
Zero Equals Extended Non-Negative Real of $p$ if and only if $p \leq 0$
Informal description
For any real number $p$, the equality $0 = \text{ofReal}(p)$ holds if and only if $p \leq 0$.
ENNReal.ofReal_lt_natCast theorem
{p : ℝ} {n : ℕ} (hn : n ≠ 0) : ENNReal.ofReal p < n ↔ p < n
Full source 
@[simp]
lemma ofReal_lt_natCast {p : ℝ} {n : ℕ} (hn : n ≠ 0) : ENNReal.ofRealENNReal.ofReal p < n ↔ p < n := by
  exact mod_cast ofReal_lt_ofReal_iff (Nat.cast_pos.2 hn.bot_lt)
Comparison of Extended Non-Negative Real with Natural Number Cast: $\text{ofReal}(p) < n \leftrightarrow p < n$
Informal description
For any real number $p$ and natural number $n$ with $n \neq 0$, the extended non-negative real number $\text{ofReal}(p)$ is less than $n$ if and only if $p < n$.
ENNReal.ofReal_lt_one theorem
{p : ℝ} : ENNReal.ofReal p < 1 ↔ p < 1
Full source 
@[simp]
lemma ofReal_lt_one {p : ℝ} : ENNReal.ofRealENNReal.ofReal p < 1 ↔ p < 1 := by
  exact mod_cast ofReal_lt_natCast one_ne_zero
Comparison of Extended Non-Negative Real with One: $\text{ofReal}(p) < 1 \leftrightarrow p < 1$
Informal description
For any real number $p$, the extended non-negative real number $\text{ofReal}(p)$ is strictly less than $1$ if and only if $p$ is strictly less than $1$.
ENNReal.ofReal_lt_ofNat theorem
{p : ℝ} {n : ℕ} [n.AtLeastTwo] : ENNReal.ofReal p < ofNat(n) ↔ p < OfNat.ofNat n
Full source 
@[simp]
lemma ofReal_lt_ofNat {p : ℝ} {n : ℕ} [n.AtLeastTwo] :
    ENNReal.ofRealENNReal.ofReal p < ofNat(n) ↔ p < OfNat.ofNat n :=
  ofReal_lt_natCast (NeZero.ne n)
Comparison of Extended Non-Negative Real with Natural Number ≥ 2: $\text{ofReal}(p) < n \leftrightarrow p < n$
Informal description
For any real number $p$ and natural number $n \geq 2$, the extended non-negative real number $\text{ofReal}(p)$ is less than $n$ if and only if $p < n$.
ENNReal.natCast_le_ofReal theorem
{n : ℕ} {p : ℝ} (hn : n ≠ 0) : n ≤ ENNReal.ofReal p ↔ n ≤ p
Full source 
@[simp]
lemma natCast_le_ofReal {n : ℕ} {p : ℝ} (hn : n ≠ 0) : n ≤ ENNReal.ofReal p ↔ n ≤ p := by
  simp only [← not_lt, ofReal_lt_natCast hn]
Comparison of Extended Non-Negative Real with Natural Number Cast: $n \leq \text{ofReal}(p) \leftrightarrow n \leq p$
Informal description
For any natural number $n \neq 0$ and real number $p$, the extended non-negative real number $\text{ofReal}(p)$ is greater than or equal to $n$ if and only if $p \geq n$.
ENNReal.one_le_ofReal theorem
{p : ℝ} : 1 ≤ ENNReal.ofReal p ↔ 1 ≤ p
Full source 
@[simp]
lemma one_le_ofReal {p : ℝ} : 1 ≤ ENNReal.ofReal p ↔ 1 ≤ p := by
  exact mod_cast natCast_le_ofReal one_ne_zero
Comparison of $\text{ENNReal.ofReal}(p)$ with $1$: $1 \leq \text{ENNReal.ofReal}(p) \leftrightarrow 1 \leq p$
Informal description
For any real number $p$, the extended non-negative real number $\text{ENNReal.ofReal}(p)$ is greater than or equal to $1$ if and only if $p \geq 1$.
ENNReal.ofNat_le_ofReal theorem
{n : ℕ} [n.AtLeastTwo] {p : ℝ} : ofNat(n) ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p
Full source 
@[simp]
lemma ofNat_le_ofReal {n : ℕ} [n.AtLeastTwo] {p : ℝ} :
    ofNat(n)ofNat(n) ≤ ENNReal.ofReal p ↔ OfNat.ofNat n ≤ p :=
  natCast_le_ofReal (NeZero.ne n)
Comparison of Extended Non-Negative Real with Numerals ≥ 2: $n \leq \text{ofReal}(p) \leftrightarrow n \leq p$
Informal description
For any natural number $n \geq 2$ and real number $p$, the extended non-negative real number $\text{ENNReal.ofReal}(p)$ is greater than or equal to $n$ if and only if $p \geq n$.
ENNReal.ofReal_le_natCast theorem
{r : ℝ} {n : ℕ} : ENNReal.ofReal r ≤ n ↔ r ≤ n
Full source 
@[simp, norm_cast]
lemma ofReal_le_natCast {r : ℝ} {n : ℕ} : ENNReal.ofRealENNReal.ofReal r ≤ n ↔ r ≤ n :=
  coe_le_coe.trans Real.toNNReal_le_natCast
Comparison of $\text{ENNReal.ofReal}(r)$ with Natural Numbers: $\text{ENNReal.ofReal}(r) \leq n \leftrightarrow r \leq n$
Informal description
For any real number $r$ and natural number $n$, the extended non-negative real number obtained from $r$ via $\text{ENNReal.ofReal}(r)$ is less than or equal to $n$ if and only if $r \leq n$.
ENNReal.ofReal_le_ofNat theorem
{r : ℝ} {n : ℕ} [n.AtLeastTwo] : ENNReal.ofReal r ≤ ofNat(n) ↔ r ≤ OfNat.ofNat n
Full source 
@[simp]
lemma ofReal_le_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
    ENNReal.ofRealENNReal.ofReal r ≤ ofNat(n) ↔ r ≤ OfNat.ofNat n :=
  ofReal_le_natCast
Comparison of Extended Non-Negative Real via `ofReal` with Numerals ≥ 2: $\text{ENNReal.ofReal}(r) \leq n \leftrightarrow r \leq n$ for $n \geq 2$
Informal description
For any real number $r$ and natural number $n \geq 2$, the extended non-negative real number obtained from $r$ via $\text{ENNReal.ofReal}(r)$ is less than or equal to $n$ if and only if $r \leq n$.
ENNReal.natCast_lt_ofReal theorem
{n : ℕ} {r : ℝ} : n < ENNReal.ofReal r ↔ n < r
Full source 
@[simp]
lemma natCast_lt_ofReal {n : ℕ} {r : ℝ} : n < ENNReal.ofReal r ↔ n < r :=
  coe_lt_coe.trans Real.natCast_lt_toNNReal
Comparison of Natural Number and Extended Non-Negative Real via `ofReal`
Informal description
For any natural number $n$ and real number $r$, the extended non-negative real number obtained by casting $n$ is less than the extended non-negative real number obtained from $r$ via `ENNReal.ofReal` if and only if $n$ is less than $r$ in the usual ordering of real numbers. In other words, $n < \text{ENNReal.ofReal}(r) \leftrightarrow n < r$.
ENNReal.one_lt_ofReal theorem
{r : ℝ} : 1 < ENNReal.ofReal r ↔ 1 < r
Full source 
@[simp]
lemma one_lt_ofReal {r : ℝ} : 1 < ENNReal.ofReal r ↔ 1 < r := coe_lt_coe.trans Real.one_lt_toNNReal
Comparison of One and Extended Non-Negative Real via `ofReal`
Informal description
For any real number $r$, the extended non-negative real number obtained by applying `ENNReal.ofReal` to $r$ is greater than $1$ if and only if $r > 1$. In other words, $1 < \text{ENNReal.ofReal}(r) \leftrightarrow 1 < r$.
ENNReal.ofNat_lt_ofReal theorem
{n : ℕ} [n.AtLeastTwo] {r : ℝ} : ofNat(n) < ENNReal.ofReal r ↔ OfNat.ofNat n < r
Full source 
@[simp]
lemma ofNat_lt_ofReal {n : ℕ} [n.AtLeastTwo] {r : ℝ} :
    ofNat(n)ofNat(n) < ENNReal.ofReal r ↔ OfNat.ofNat n < r :=
  natCast_lt_ofReal
Comparison of Numerals ≥ 2 and Extended Non-Negative Reals via `ofReal`
Informal description
For any natural number $n \geq 2$ and real number $r$, the extended non-negative real number obtained from the numeral $n$ is less than the extended non-negative real number obtained from $r$ via `ENNReal.ofReal` if and only if $n$ is less than $r$ in the usual ordering of real numbers. In other words, $n < \text{ENNReal.ofReal}(r) \leftrightarrow n < r$.
ENNReal.ofReal_eq_natCast theorem
{r : ℝ} {n : ℕ} (h : n ≠ 0) : ENNReal.ofReal r = n ↔ r = n
Full source 
@[simp]
lemma ofReal_eq_natCast {r : ℝ} {n : ℕ} (h : n ≠ 0) : ENNReal.ofRealENNReal.ofReal r = n ↔ r = n :=
  ENNReal.coe_inj.trans <| Real.toNNReal_eq_natCast h
$\text{ofReal}(r) = n \leftrightarrow r = n$ for $n \neq 0$
Informal description
For any real number $r$ and any natural number $n \neq 0$, the extended non-negative real number $\text{ofReal}(r)$ equals $n$ if and only if $r = n$, where $\text{ofReal}(r)$ maps $r$ to $0$ if $r$ is negative and to $r$ otherwise.
ENNReal.ofReal_eq_ofNat theorem
{r : ℝ} {n : ℕ} [n.AtLeastTwo] : ENNReal.ofReal r = ofNat(n) ↔ r = OfNat.ofNat n
Full source 
@[simp]
lemma ofReal_eq_ofNat {r : ℝ} {n : ℕ} [n.AtLeastTwo] :
    ENNReal.ofRealENNReal.ofReal r = ofNat(n) ↔ r = OfNat.ofNat n :=
  ofReal_eq_natCast (NeZero.ne n)
$\text{ofReal}(r) = n \leftrightarrow r = n$ for natural numbers $n \geq 2$
Informal description
For any real number $r$ and any natural number $n \geq 2$, the extended non-negative real number $\text{ofReal}(r)$ equals the canonical embedding of $n$ if and only if $r$ equals the canonical embedding of $n$ in the reals. Here, $\text{ofReal}(r)$ maps $r$ to $0$ if $r$ is negative and to $r$ otherwise.
ENNReal.ofReal_le_iff_le_toReal theorem
{a : ℝ} {b : ℝ≥0∞} (hb : b ≠ ∞) : ENNReal.ofReal a ≤ b ↔ a ≤ ENNReal.toReal b
Full source 
theorem ofReal_le_iff_le_toReal {a : ℝ} {b : ℝ≥0∞} (hb : b ≠ ∞) :
    ENNReal.ofRealENNReal.ofReal a ≤ b ↔ a ≤ ENNReal.toReal b := by
  lift b to ℝ≥0 using hb
  simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_le_iff_le_coe
Inequality between $\text{ofReal}(a)$ and $b$ is equivalent to $a \leq \text{toReal}(b)$ for finite $b$
Informal description
For any real number $a$ and any extended non-negative real number $b \neq \infty$, the inequality $\text{ofReal}(a) \leq b$ holds if and only if $a \leq \text{toReal}(b)$, where $\text{ofReal}(a)$ is the extended non-negative real number obtained from $a$ (mapping negative $a$ to $0$), and $\text{toReal}(b)$ is the real number obtained from $b$ (mapping $\infty$ to $0$ if $b = \infty$).
ENNReal.ofReal_lt_iff_lt_toReal theorem
{a : ℝ} {b : ℝ≥0∞} (ha : 0 ≤ a) (hb : b ≠ ∞) : ENNReal.ofReal a < b ↔ a < ENNReal.toReal b
Full source 
theorem ofReal_lt_iff_lt_toReal {a : ℝ} {b : ℝ≥0∞} (ha : 0 ≤ a) (hb : b ≠ ∞) :
    ENNReal.ofRealENNReal.ofReal a < b ↔ a < ENNReal.toReal b := by
  lift b to ℝ≥0 using hb
  simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_lt_iff_lt_coe ha
Inequality $\text{ofReal}(a) < b$ iff $a < \text{toReal}(b)$ for $a \geq 0$ and finite $b$
Informal description
For any real number $a \geq 0$ and any finite extended non-negative real number $b \neq \infty$, the inequality $\text{ENNReal.ofReal}(a) < b$ holds if and only if $a < \text{ENNReal.toReal}(b)$, where $\text{ENNReal.ofReal}(a)$ maps $a$ to the extended non-negative reals (with negative values mapped to $0$) and $\text{ENNReal.toReal}(b)$ maps $b$ back to a real number (with $\infty$ mapped to $0$).
ENNReal.ofReal_lt_coe_iff theorem
{a : ℝ} {b : ℝ≥0} (ha : 0 ≤ a) : ENNReal.ofReal a < b ↔ a < b
Full source 
theorem ofReal_lt_coe_iff {a : ℝ} {b : ℝ≥0} (ha : 0 ≤ a) : ENNReal.ofRealENNReal.ofReal a < b ↔ a < b :=
  (ofReal_lt_iff_lt_toReal ha coe_ne_top).trans <| by rw [coe_toReal]
Inequality $\text{ofReal}(a) < b$ iff $a < b$ for non-negative $a$ and $b$
Informal description
For any real number $a \geq 0$ and any non-negative real number $b$ (interpreted as an element of $\mathbb{R}_{\geq 0}$), the inequality $\text{ENNReal.ofReal}(a) < b$ holds if and only if $a < b$.
ENNReal.le_ofReal_iff_toReal_le theorem
{a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ∞) (hb : 0 ≤ b) : a ≤ ENNReal.ofReal b ↔ ENNReal.toReal a ≤ b
Full source 
theorem le_ofReal_iff_toReal_le {a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ∞) (hb : 0 ≤ b) :
    a ≤ ENNReal.ofReal b ↔ ENNReal.toReal a ≤ b := by
  lift a to ℝ≥0 using ha
  simpa [ENNReal.ofReal, ENNReal.toReal] using Real.le_toNNReal_iff_coe_le hb
Inequality $a \leq \text{ofReal}(b)$ iff $\text{toReal}(a) \leq b$ for finite $a$ and non-negative $b$
Informal description
For any finite extended non-negative real number $a \neq \infty$ and any non-negative real number $b \geq 0$, the inequality $a \leq \text{ENNReal.ofReal}(b)$ holds if and only if $\text{ENNReal.toReal}(a) \leq b$, where $\text{ENNReal.ofReal}(b)$ maps $b$ to the extended non-negative reals (with negative values mapped to $0$) and $\text{ENNReal.toReal}(a)$ maps $a$ back to a real number (with $\infty$ mapped to $0$).
ENNReal.toReal_le_of_le_ofReal theorem
{a : ℝ≥0∞} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ENNReal.ofReal b) : ENNReal.toReal a ≤ b
Full source 
theorem toReal_le_of_le_ofReal {a : ℝ≥0∞} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ENNReal.ofReal b) :
    ENNReal.toReal a ≤ b :=
  have ha : a ≠ ∞ := ne_top_of_le_ne_top ofReal_ne_top h
  (le_ofReal_iff_toReal_le ha hb).1 h
Inequality Preservation from Extended to Standard Non-Negative Reals: $a \leq \text{ofReal}(b) \to \text{toReal}(a) \leq b$ for $b \geq 0$
Informal description
For any extended non-negative real number $a$ and any real number $b \geq 0$, if $a \leq \text{ENNReal.ofReal}(b)$, then $\text{ENNReal.toReal}(a) \leq b$.
ENNReal.lt_ofReal_iff_toReal_lt theorem
{a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ∞) : a < ENNReal.ofReal b ↔ ENNReal.toReal a < b
Full source 
theorem lt_ofReal_iff_toReal_lt {a : ℝ≥0∞} {b : ℝ} (ha : a ≠ ∞) :
    a < ENNReal.ofReal b ↔ ENNReal.toReal a < b := by
  lift a to ℝ≥0 using ha
  simpa [ENNReal.ofReal, ENNReal.toReal] using Real.lt_toNNReal_iff_coe_lt
Strict Inequality Comparison between Extended and Standard Non-Negative Reals
Informal description
For any extended non-negative real number $a \neq \infty$ and any real number $b$, the inequality $a < \text{ENNReal.ofReal}(b)$ holds if and only if $\text{ENNReal.toReal}(a) < b$, where $\text{ENNReal.ofReal}(b)$ maps $b$ to the extended non-negative reals (with negative values mapped to $0$) and $\text{ENNReal.toReal}(a)$ maps $a$ back to a real number (with $\infty$ mapped to $0$).
ENNReal.toReal_lt_of_lt_ofReal theorem
{b : ℝ} (h : a < ENNReal.ofReal b) : ENNReal.toReal a < b
Full source 
theorem toReal_lt_of_lt_ofReal {b : ℝ} (h : a < ENNReal.ofReal b) : ENNReal.toReal a < b :=
  (lt_ofReal_iff_toReal_lt h.ne_top).1 h
Strict Inequality Preservation from Extended to Standard Non-Negative Reals
Informal description
For any extended non-negative real number $a$ and any real number $b$, if $a$ is strictly less than the extended non-negative real number obtained by applying $\text{ENNReal.ofReal}$ to $b$, then the real number obtained by applying $\text{ENNReal.toReal}$ to $a$ is strictly less than $b$.
ENNReal.ofReal_mul theorem
{p q : ℝ} (hp : 0 ≤ p) : ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
Full source 
theorem ofReal_mul {p q : ℝ} (hp : 0 ≤ p) :
    ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q := by
  simp only [ENNReal.ofReal, ← coe_mul, Real.toNNReal_mul hp]
Multiplicativity of `ofReal` for Non-Negative Reals
Informal description
For any real numbers $p$ and $q$ with $p \geq 0$, the extended non-negative real number obtained by applying the `ofReal` function to the product $p \cdot q$ is equal to the product of the `ofReal` images of $p$ and $q$, i.e., \[ \text{ofReal}(p \cdot q) = \text{ofReal}(p) \cdot \text{ofReal}(q). \]
ENNReal.ofReal_mul' theorem
{p q : ℝ} (hq : 0 ≤ q) : ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q
Full source 
theorem ofReal_mul' {p q : ℝ} (hq : 0 ≤ q) :
    ENNReal.ofReal (p * q) = ENNReal.ofReal p * ENNReal.ofReal q := by
  rw [mul_comm, ofReal_mul hq, mul_comm]
Multiplicativity of `ofReal` for Non-Negative Second Argument
Informal description
For any real numbers $p$ and $q$ with $q \geq 0$, the extended non-negative real number obtained by applying the `ofReal` function to the product $p \cdot q$ is equal to the product of the `ofReal` images of $p$ and $q$, i.e., \[ \text{ofReal}(p \cdot q) = \text{ofReal}(p) \cdot \text{ofReal}(q). \]
ENNReal.ofReal_pow theorem
{p : ℝ} (hp : 0 ≤ p) (n : ℕ) : ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n
Full source 
theorem ofReal_pow {p : ℝ} (hp : 0 ≤ p) (n : ℕ) :
    ENNReal.ofReal (p ^ n) = ENNReal.ofReal p ^ n := by
  rw [ofReal_eq_coe_nnreal hp, ← coe_pow, ← ofReal_coe_nnreal, NNReal.coe_pow, NNReal.coe_mk]
Power Preservation of `ofReal` for Non-Negative Reals
Informal description
For any real number $p \geq 0$ and natural number $n$, the extended non-negative real number obtained by applying the `ofReal` function to $p^n$ is equal to the $n$-th power of the extended non-negative real number obtained by applying `ofReal` to $p$. That is, \[ \text{ofReal}(p^n) = (\text{ofReal}\, p)^n. \]
ENNReal.ofReal_nsmul theorem
{x : ℝ} {n : ℕ} : ENNReal.ofReal (n • x) = n • ENNReal.ofReal x
Full source 
theorem ofReal_nsmul {x : ℝ} {n : ℕ} : ENNReal.ofReal (n • x) = n • ENNReal.ofReal x := by
  simp only [nsmul_eq_mul, ← ofReal_natCast n, ← ofReal_mul n.cast_nonneg]
Scalar Multiplication Preservation of `ofReal` for Natural Numbers
Informal description
For any real number $x$ and natural number $n$, the extended non-negative real number obtained by applying the `ofReal` function to the scalar multiple $n \cdot x$ is equal to the scalar multiple of the extended non-negative real number obtained by applying `ofReal` to $x$. That is, \[ \text{ofReal}(n \cdot x) = n \cdot \text{ofReal}(x). \]
ENNReal.toNNReal_mul theorem
{a b : ℝ≥0∞} : (a * b).toNNReal = a.toNNReal * b.toNNReal
Full source 
@[simp]
theorem toNNReal_mul {a b : ℝ≥0∞} : (a * b).toNNReal = a.toNNReal * b.toNNReal :=
  WithTop.untopD_zero_mul a b
Multiplicativity of Non-Negative Real Part for Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$, the non-negative real part of their product equals the product of their non-negative real parts, i.e., \[ \text{toNNReal}(a \cdot b) = \text{toNNReal}(a) \cdot \text{toNNReal}(b). \]
ENNReal.toNNReal_mul_top theorem
(a : ℝ≥0∞) : ENNReal.toNNReal (a * ∞) = 0
Full source 
theorem toNNReal_mul_top (a : ℝ≥0∞) : ENNReal.toNNReal (a * ∞) = 0 := by simp
Vanishing of Non-Negative Real Part under Multiplication by Infinity
Informal description
For any extended non-negative real number $a$, the non-negative real part of the product $a \cdot \infty$ is zero, i.e., \[ \text{toNNReal}(a \cdot \infty) = 0. \]
ENNReal.toNNReal_top_mul theorem
(a : ℝ≥0∞) : ENNReal.toNNReal (∞ * a) = 0
Full source 
theorem toNNReal_top_mul (a : ℝ≥0∞) : ENNReal.toNNReal (∞ * a) = 0 := by simp
Non-Negative Real Part of Infinity Multiplied by Extended Non-Negative Real is Zero
Informal description
For any extended non-negative real number $a$, the non-negative real part of the product $\infty \cdot a$ is equal to $0$, i.e., \[ \text{toNNReal}(\infty \cdot a) = 0. \]
ENNReal.toNNRealHom definition
: ℝ≥0∞ →*₀ ℝ≥0
Full source 
/-- `ENNReal.toNNReal` as a `MonoidHom`. -/
def toNNRealHom : ℝ≥0∞ℝ≥0∞ →*₀ ℝ≥0 where
  toFun := ENNReal.toNNReal
  map_one' := toNNReal_coe _
  map_mul' _ _ := toNNReal_mul
  map_zero' := toNNReal_zero
Monoid homomorphism from extended non-negative reals to non-negative reals
Informal description
The monoid homomorphism from the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ to the non-negative real numbers $\mathbb{R}_{\geq 0}$, mapping each element to its non-negative real part. This homomorphism preserves multiplication, zero, and one, with the following properties: - $\text{toNNRealHom}(1) = 1$ - $\text{toNNRealHom}(a \cdot b) = \text{toNNRealHom}(a) \cdot \text{toNNRealHom}(b)$ for any $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ - $\text{toNNRealHom}(0) = 0$
ENNReal.toNNReal_pow theorem
(a : ℝ≥0∞) (n : ℕ) : (a ^ n).toNNReal = a.toNNReal ^ n
Full source 
@[simp]
theorem toNNReal_pow (a : ℝ≥0∞) (n : ℕ) : (a ^ n).toNNReal = a.toNNReal ^ n :=
  toNNRealHom.map_pow a n
Power Preservation under Non-Negative Real Part: $\text{toNNReal}(a^n) = (\text{toNNReal}(a))^n$
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any natural number $n \in \mathbb{N}$, the non-negative real part of $a^n$ is equal to the $n$-th power of the non-negative real part of $a$, i.e., \[ \text{toNNReal}(a^n) = (\text{toNNReal}(a))^n. \]
ENNReal.toRealHom definition
: ℝ≥0∞ →*₀ ℝ
Full source 
/-- `ENNReal.toReal` as a `MonoidHom`. -/
def toRealHom : ℝ≥0∞ℝ≥0∞ →*₀ ℝ :=
  (NNReal.toRealHom : ℝ≥0ℝ≥0 →*₀ ℝ).comp toNNRealHom
Monoid homomorphism from extended non-negative reals to reals
Informal description
The monoid homomorphism from the extended non-negative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$ to the real numbers $\mathbb{R}$, obtained by composing the monoid homomorphism from extended non-negative reals to non-negative reals with the canonical inclusion of non-negative reals into reals. This homomorphism preserves multiplication, zero, and one, with the following properties: - $\text{toRealHom}(1) = 1$ - $\text{toRealHom}(a \cdot b) = \text{toRealHom}(a) \cdot \text{toRealHom}(b)$ for any $a, b \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ - $\text{toRealHom}(0) = 0$
ENNReal.toReal_mul theorem
: (a * b).toReal = a.toReal * b.toReal
Full source 
@[simp]
theorem toReal_mul : (a * b).toReal = a.toReal * b.toReal :=
  toRealHom.map_mul a b
Multiplicativity of Real Conversion for Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$, the real-valued conversion of their product equals the product of their real-valued conversions, i.e., $(a \cdot b).\text{toReal} = a.\text{toReal} \cdot b.\text{toReal}$.
ENNReal.toReal_nsmul theorem
(a : ℝ≥0∞) (n : ℕ) : (n • a).toReal = n • a.toReal
Full source 
theorem toReal_nsmul (a : ℝ≥0∞) (n : ℕ) : (n • a).toReal = n • a.toReal := by simp
Scalar Multiplication Preservation under Extended Non-Negative Real to Real Conversion: $(n \cdot a).\text{toReal} = n \cdot a.\text{toReal}$
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any natural number $n$, the real number obtained by applying the `toReal` function to the $n$-th multiple of $a$ under scalar multiplication equals the $n$-th multiple of the real number obtained by applying `toReal` to $a$, i.e., $(n \cdot a).\text{toReal} = n \cdot a.\text{toReal}$.
ENNReal.toReal_pow theorem
(a : ℝ≥0∞) (n : ℕ) : (a ^ n).toReal = a.toReal ^ n
Full source 
@[simp]
theorem toReal_pow (a : ℝ≥0∞) (n : ℕ) : (a ^ n).toReal = a.toReal ^ n :=
  toRealHom.map_pow a n
Power Preservation under Extended Non-Negative Real to Real Conversion: $\text{toReal}(a^n) = \text{toReal}(a)^n$
Informal description
For any extended non-negative real number $a \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any natural number $n$, the real number obtained by applying the `toReal` function to $a^n$ is equal to the $n$-th power of the real number obtained by applying `toReal` to $a$, i.e., $\text{toReal}(a^n) = (\text{toReal}(a))^n$.
ENNReal.toReal_ofReal_mul theorem
(c : ℝ) (a : ℝ≥0∞) (h : 0 ≤ c) : ENNReal.toReal (ENNReal.ofReal c * a) = c * ENNReal.toReal a
Full source 
theorem toReal_ofReal_mul (c : ℝ) (a : ℝ≥0∞) (h : 0 ≤ c) :
    ENNReal.toReal (ENNReal.ofReal c * a) = c * ENNReal.toReal a := by
  rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal h]
Real Conversion of Scaled Extended Non-Negative Real: $\text{toReal}(\text{ofReal}(c) \cdot a) = c \cdot \text{toReal}(a)$
Informal description
For any real number $c \geq 0$ and any extended non-negative real number $a$, the real-valued conversion of the product $\text{ofReal}(c) \cdot a$ equals $c$ multiplied by the real-valued conversion of $a$, i.e., $\text{toReal}(\text{ofReal}(c) \cdot a) = c \cdot \text{toReal}(a)$.
ENNReal.toReal_mul_top theorem
(a : ℝ≥0∞) : ENNReal.toReal (a * ∞) = 0
Full source 
theorem toReal_mul_top (a : ℝ≥0∞) : ENNReal.toReal (a * ∞) = 0 := by
  rw [toReal_mul, toReal_top, mul_zero]
Real Conversion of Extended Non-Negative Real Multiplied by Infinity is Zero
Informal description
For any extended non-negative real number $a$, the real-valued conversion of $a \cdot \infty$ is equal to $0$, i.e., $\text{toReal}(a \cdot \infty) = 0$.
ENNReal.toReal_top_mul theorem
(a : ℝ≥0∞) : ENNReal.toReal (∞ * a) = 0
Full source 
theorem toReal_top_mul (a : ℝ≥0∞) : ENNReal.toReal (∞ * a) = 0 := by
  rw [mul_comm]
  exact toReal_mul_top _
Real Conversion of Infinity Multiplied by Extended Non-Negative Real is Zero
Informal description
For any extended non-negative real number $a$, the real-valued conversion of $\infty \cdot a$ is equal to $0$, i.e., $\text{toReal}(\infty \cdot a) = 0$.
ENNReal.toReal_eq_toReal theorem
(ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal = b.toReal ↔ a = b
Full source 
theorem toReal_eq_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal = b.toReal ↔ a = b := by
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  simp only [coe_inj, NNReal.coe_inj, coe_toReal]
Equality of Extended Non-Negative Reals via Real Projection
Informal description
For any extended non-negative real numbers $a$ and $b$ such that $a \neq \infty$ and $b \neq \infty$, the equality of their real-valued projections $a.\text{toReal} = b.\text{toReal}$ holds if and only if $a = b$.
ENNReal.trichotomy theorem
(p : ℝ≥0∞) : p = 0 ∨ p = ∞ ∨ 0 < p.toReal
Full source 
protected theorem trichotomy (p : ℝ≥0∞) : p = 0 ∨ p = ∞ ∨ 0 < p.toReal := by
  simpa only [or_iff_not_imp_left] using toReal_pos
Trichotomy for Extended Non-Negative Real Numbers
Informal description
For any extended non-negative real number $p \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, exactly one of the following holds: $p = 0$, $p = \infty$, or $0 < p_{\text{toReal}}$ (where $p_{\text{toReal}}$ is the real-valued projection of $p$).
ENNReal.trichotomy₂ theorem
{p q : ℝ≥0∞} (hpq : p ≤ q) : p = 0 ∧ q = 0 ∨ p = 0 ∧ q = ∞ ∨ p = 0 ∧ 0 < q.toReal ∨ p = ∞ ∧ q = ∞ ∨ 0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal
Full source 
protected theorem trichotomy₂ {p q : ℝ≥0∞} (hpq : p ≤ q) :
    p = 0 ∧ q = 0p = 0 ∧ q = 0 ∨
      p = 0 ∧ q = ∞ ∨
        p = 0 ∧ 0 < q.toReal ∨
          p = ∞ ∧ q = ∞ ∨
            0 < p.toReal ∧ q = ∞ ∨ 0 < p.toReal ∧ 0 < q.toReal ∧ p.toReal ≤ q.toReal := by
  rcases eq_or_lt_of_le (bot_le : 0 ≤ p) with ((rfl : 0 = p) | (hp : 0 < p))
  · simpa using q.trichotomy
  rcases eq_or_lt_of_le (le_top : q ≤ ∞) with (rfl | hq)
  · simpa using p.trichotomy
  repeat' right
  have hq' : 0 < q := lt_of_lt_of_le hp hpq
  have hp' : p < ∞ := lt_of_le_of_lt hpq hq
  simp [ENNReal.toReal_mono hq.ne hpq, ENNReal.toReal_pos_iff, hp, hp', hq', hq]
Extended Trichotomy for Ordered Pairs of Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $p$ and $q$ such that $p \leq q$, exactly one of the following holds: 1. $p = 0$ and $q = 0$, or 2. $p = 0$ and $q = \infty$, or 3. $p = 0$ and $0 < q_{\text{toReal}}$, or 4. $p = \infty$ and $q = \infty$, or 5. $0 < p_{\text{toReal}}$ and $q = \infty$, or 6. $0 < p_{\text{toReal}}$ and $0 < q_{\text{toReal}}$ with $p_{\text{toReal}} \leq q_{\text{toReal}}$. Here, $p_{\text{toReal}}$ denotes the real-valued projection of $p$.
ENNReal.dichotomy theorem
(p : ℝ≥0∞) [Fact (1 ≤ p)] : p = ∞ ∨ 1 ≤ p.toReal
Full source 
protected theorem dichotomy (p : ℝ≥0∞) [Fact (1 ≤ p)] : p = ∞ ∨ 1 ≤ p.toReal :=
  haveI : p = ⊤ ∨ 0 < p.toReal ∧ 1 ≤ p.toReal := by
    simpa using ENNReal.trichotomy₂ (Fact.out : 1 ≤ p)
  this.imp_right fun h => h.2
Dichotomy for Extended Non-Negative Reals with Lower Bound 1
Informal description
For any extended non-negative real number $p \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ satisfying $1 \leq p$, either $p = \infty$ or the real-valued projection of $p$ satisfies $1 \leq p_{\text{toReal}}$.
ENNReal.toReal_pos_iff_ne_top theorem
(p : ℝ≥0∞) [Fact (1 ≤ p)] : 0 < p.toReal ↔ p ≠ ∞
Full source 
theorem toReal_pos_iff_ne_top (p : ℝ≥0∞) [Fact (1 ≤ p)] : 0 < p.toReal ↔ p ≠ ∞ :=
  ⟨fun h hp =>
    have : (0 : ℝ) ≠ 0 := toReal_top ▸ (hp ▸ h.ne : 0 ≠ ∞.toReal)
    this rfl,
    fun h => zero_lt_one.trans_le (p.dichotomy.resolve_left h)⟩
Positivity of Extended Non-Negative Real Projection Equivalent to Finiteness
Informal description
For any extended non-negative real number $p \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $1 \leq p$, the real-valued projection $p_{\text{toReal}}$ is strictly positive if and only if $p$ is not equal to $\infty$.
ENNReal.toNNReal_iInf theorem
(hf : ∀ i, f i ≠ ∞) : (iInf f).toNNReal = ⨅ i, (f i).toNNReal
Full source 
theorem toNNReal_iInf (hf : ∀ i, f i ≠ ∞) : (iInf f).toNNReal = ⨅ i, (f i).toNNReal := by
  cases isEmpty_or_nonempty ι
  · rw [iInf_of_empty, toNNReal_top, NNReal.iInf_empty]
  · lift f to ι → ℝ≥0 using hf
    simp_rw [← coe_iInf, toNNReal_coe]
Non-negative real part of infimum equals infimum of non-negative real parts
Informal description
For any indexed family of extended non-negative real numbers $f : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $f_i \neq \infty$ for all $i$, the non-negative real part of the infimum of $f$ is equal to the infimum of the non-negative real parts of $f_i$. In other words, \[ \left(\bigsqcap_i f_i\right)_{\text{toNNReal}} = \bigsqcap_i (f_i)_{\text{toNNReal}}. \]
ENNReal.toNNReal_sInf theorem
(s : Set ℝ≥0∞) (hs : ∀ r ∈ s, r ≠ ∞) : (sInf s).toNNReal = sInf (ENNReal.toNNReal '' s)
Full source 
theorem toNNReal_sInf (s : Set ℝ≥0∞) (hs : ∀ r ∈ s, r ≠ ∞) :
    (sInf s).toNNReal = sInf (ENNReal.toNNRealENNReal.toNNReal '' s) := by
  have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
  simpa only [← sInf_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iInf hf)
Infimum Commutes with Non-Negative Real Part for Extended Non-Negative Reals
Informal description
For any set $s$ of extended non-negative real numbers (i.e., $s \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$) such that every element $r \in s$ satisfies $r \neq \infty$, the non-negative real part of the infimum of $s$ is equal to the infimum of the non-negative real parts of the elements in $s$. In other words, \[ (\inf s)_{\text{toNNReal}} = \inf \{r_{\text{toNNReal}} \mid r \in s\}. \]
ENNReal.toNNReal_iSup theorem
(hf : ∀ i, f i ≠ ∞) : (iSup f).toNNReal = ⨆ i, (f i).toNNReal
Full source 
theorem toNNReal_iSup (hf : ∀ i, f i ≠ ∞) : (iSup f).toNNReal = ⨆ i, (f i).toNNReal := by
  lift f to ι → ℝ≥0 using hf
  simp_rw [toNNReal_coe]
  by_cases h : BddAbove (range f)
  · rw [← coe_iSup h, toNNReal_coe]
  · rw [NNReal.iSup_of_not_bddAbove h, iSup_coe_eq_top.2 h, toNNReal_top]
Non-negative real part of supremum equals supremum of non-negative real parts
Informal description
For any indexed family of extended non-negative real numbers $f : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $f_i \neq \infty$ for all $i$, the non-negative real part of the supremum of $f$ is equal to the supremum of the non-negative real parts of $f_i$. In other words, \[ \left(\bigsqcup_i f_i\right)_{\text{toNNReal}} = \bigsqcup_i (f_i)_{\text{toNNReal}}. \]
ENNReal.toNNReal_sSup theorem
(s : Set ℝ≥0∞) (hs : ∀ r ∈ s, r ≠ ∞) : (sSup s).toNNReal = sSup (ENNReal.toNNReal '' s)
Full source 
theorem toNNReal_sSup (s : Set ℝ≥0∞) (hs : ∀ r ∈ s, r ≠ ∞) :
    (sSup s).toNNReal = sSup (ENNReal.toNNRealENNReal.toNNReal '' s) := by
  have hf : ∀ i, ((↑) : s → ℝ≥0∞) i ≠ ∞ := fun ⟨r, rs⟩ => hs r rs
  simpa only [← sSup_range, ← image_eq_range, Subtype.range_coe_subtype] using (toNNReal_iSup hf)
Supremum Commutes with Non-Negative Real Part for Extended Non-Negative Reals
Informal description
For any set $s$ of extended non-negative real numbers (i.e., $s \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$) such that every element $r \in s$ satisfies $r \neq \infty$, the non-negative real part of the supremum of $s$ is equal to the supremum of the non-negative real parts of the elements in $s$. In other words, \[ (\sup s)_{\text{toNNReal}} = \sup \{r_{\text{toNNReal}} \mid r \in s\}. \]
ENNReal.toReal_iInf theorem
(hf : ∀ i, f i ≠ ∞) : (iInf f).toReal = ⨅ i, (f i).toReal
Full source 
theorem toReal_iInf (hf : ∀ i, f i ≠ ∞) : (iInf f).toReal = ⨅ i, (f i).toReal := by
  simp only [ENNReal.toReal, toNNReal_iInf hf, NNReal.coe_iInf]
Real part of infimum equals infimum of real parts for extended non-negative reals
Informal description
For any indexed family of extended non-negative real numbers $f : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $f_i \neq \infty$ for all $i$, the real part of the infimum of $f$ is equal to the infimum of the real parts of $f_i$. In other words, \[ \left(\bigsqcap_i f_i\right)_{\text{toReal}} = \bigsqcap_i (f_i)_{\text{toReal}}. \]
ENNReal.toReal_sInf theorem
(s : Set ℝ≥0∞) (hf : ∀ r ∈ s, r ≠ ∞) : (sInf s).toReal = sInf (ENNReal.toReal '' s)
Full source 
theorem toReal_sInf (s : Set ℝ≥0∞) (hf : ∀ r ∈ s, r ≠ ∞) :
    (sInf s).toReal = sInf (ENNReal.toRealENNReal.toReal '' s) := by
  simp only [ENNReal.toReal, toNNReal_sInf s hf, NNReal.coe_sInf, Set.image_image]
Infimum Commutes with Real Part for Extended Non-Negative Reals
Informal description
For any set $s$ of extended non-negative real numbers (i.e., $s \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$) such that every element $r \in s$ satisfies $r \neq \infty$, the real part of the infimum of $s$ is equal to the infimum of the real parts of the elements in $s$. In other words, \[ (\inf s)_{\text{toReal}} = \inf \{r_{\text{toReal}} \mid r \in s\}. \]
ENNReal.toReal_iSup theorem
(hf : ∀ i, f i ≠ ∞) : (iSup f).toReal = ⨆ i, (f i).toReal
Full source 
theorem toReal_iSup (hf : ∀ i, f i ≠ ∞) : (iSup f).toReal = ⨆ i, (f i).toReal := by
  simp only [ENNReal.toReal, toNNReal_iSup hf, NNReal.coe_iSup]
Real part of supremum equals supremum of real parts for extended non-negative reals
Informal description
For any indexed family of extended non-negative real numbers $f : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $f_i \neq \infty$ for all $i$, the real part of the supremum of $f$ is equal to the supremum of the real parts of $f_i$. In other words, \[ \left(\bigsqcup_i f_i\right)_{\text{toReal}} = \bigsqcup_i (f_i)_{\text{toReal}}. \]
ENNReal.toReal_sSup theorem
(s : Set ℝ≥0∞) (hf : ∀ r ∈ s, r ≠ ∞) : (sSup s).toReal = sSup (ENNReal.toReal '' s)
Full source 
theorem toReal_sSup (s : Set ℝ≥0∞) (hf : ∀ r ∈ s, r ≠ ∞) :
    (sSup s).toReal = sSup (ENNReal.toRealENNReal.toReal '' s) := by
  simp only [ENNReal.toReal, toNNReal_sSup s hf, NNReal.coe_sSup, Set.image_image]
Supremum Commutes with Real Part for Extended Non-Negative Reals
Informal description
For any set $s$ of extended non-negative real numbers (i.e., $s \subseteq \mathbb{R}_{\geq 0} \cup \{\infty\}$) such that every element $r \in s$ satisfies $r \neq \infty$, the real part of the supremum of $s$ is equal to the supremum of the real parts of the elements in $s$. In other words, \[ (\sup s)_{\text{toReal}} = \sup \{r_{\text{toReal}} \mid r \in s\}. \]
ENNReal.ofReal_iInf theorem
[Nonempty ι] (f : ι → ℝ) : ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)
Full source 
@[simp] lemma ofReal_iInf [Nonempty ι] (f : ι → ℝ) :
    ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i) := by
  obtain ⟨i, hi⟩ | h := em (∃ i, f i ≤ 0)
  · rw [(iInf_eq_bot _).2 fun _ _ ↦ ⟨i, by simpa [ofReal_of_nonpos hi]⟩]
    simp [Real.iInf_nonpos' ⟨i, hi⟩]
  replace h i : 0 ≤ f i := le_of_not_le fun hi ↦ h ⟨i, hi⟩
  refine eq_of_forall_le_iff fun a ↦ ?_
  obtain rfl | ha := eq_or_ne a ∞
  · simp
  rw [le_iInf_iff, le_ofReal_iff_toReal_le ha, le_ciInf_iff ⟨0, by simpa [mem_lowerBounds]⟩]
  · exact forall_congr' fun i ↦ (le_ofReal_iff_toReal_le ha (h _)).symm
  · exact Real.iInf_nonneg h
Infimum Preservation under `ofReal`: $\text{ofReal}(\bigsqcap_i f_i) = \bigsqcap_i \text{ofReal}(f_i)$
Informal description
For any nonempty index set $\iota$ and any family of real numbers $f : \iota \to \mathbb{R}$, the extended non-negative real number obtained by applying the `ofReal` function to the infimum of $f$ is equal to the infimum of the family obtained by applying `ofReal` to each element of $f$, i.e., \[ \text{ENNReal.ofReal}\left(\bigsqcap_{i} f_i\right) = \bigsqcap_{i} \text{ENNReal.ofReal}(f_i). \] Here, `ENNReal.ofReal` maps a real number to the extended non-negative reals (with negative values mapped to $0$).
ENNReal.iInf_add theorem
: iInf f + a = ⨅ i, f i + a
Full source 
theorem iInf_add : iInf f + a = ⨅ i, f i + a :=
  le_antisymm (le_iInf fun _ => add_le_add (iInf_le _ _) <| le_rfl)
    (tsub_le_iff_right.1 <| le_iInf fun _ => tsub_le_iff_right.2 <| iInf_le _ _)
Infimum Addition Law for Extended Non-Negative Reals: $(\bigsqcap_i f_i) + a = \bigsqcap_i (f_i + a)$
Informal description
For any indexed family of extended non-negative real numbers $f : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any extended non-negative real number $a$, the sum of the infimum of $f$ and $a$ equals the infimum of the family obtained by adding $a$ to each element of $f$, i.e., \[ \left(\bigsqcap_i f_i\right) + a = \bigsqcap_i (f_i + a). \]
ENNReal.iSup_sub theorem
: (⨆ i, f i) - a = ⨆ i, f i - a
Full source 
theorem iSup_sub : (⨆ i, f i) - a = ⨆ i, f i - a :=
  le_antisymm (tsub_le_iff_right.2 <| iSup_le fun i => tsub_le_iff_right.1 <| le_iSup (f · - a) i)
    (iSup_le fun _ => tsub_le_tsub (le_iSup _ _) (le_refl a))
Supremum Subtraction Law for Extended Non-Negative Reals: $(\bigsqcup_i f_i) - a = \bigsqcup_i (f_i - a)$
Informal description
For any indexed family of extended non-negative real numbers $f : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ and any extended non-negative real number $a$, the difference between the supremum of $f$ and $a$ equals the supremum of the family obtained by subtracting $a$ from each element of $f$, i.e., \[ \left(\bigsqcup_i f_i\right) - a = \bigsqcup_i (f_i - a). \]
ENNReal.sub_iInf theorem
: (a - ⨅ i, f i) = ⨆ i, a - f i
Full source 
theorem sub_iInf : (a - ⨅ i, f i) = ⨆ i, a - f i := by
  refine eq_of_forall_ge_iff fun c => ?_
  rw [tsub_le_iff_right, add_comm, iInf_add]
  simp [tsub_le_iff_right, sub_eq_add_neg, add_comm]
Subtraction-Infimum Identity for Extended Non-Negative Reals: $a - \bigsqcap_i f_i = \bigsqcup_i (a - f_i)$
Informal description
For any extended non-negative real number $a$ and any indexed family of extended non-negative real numbers $f : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, the difference between $a$ and the infimum of $f$ equals the supremum of the family obtained by subtracting each element of $f$ from $a$, i.e., \[ a - \left(\bigsqcap_i f_i\right) = \bigsqcup_i (a - f_i). \]
ENNReal.sInf_add theorem
{s : Set ℝ≥0∞} : sInf s + a = ⨅ b ∈ s, b + a
Full source 
theorem sInf_add {s : Set ℝ≥0∞} : sInf s + a = ⨅ b ∈ s, b + a := by simp [sInf_eq_iInf, iInf_add]
Infimum Addition Law for Extended Non-Negative Reals: $\inf s + a = \inf_{b \in s} (b + a)$
Informal description
For any set $s$ of extended non-negative real numbers and any extended non-negative real number $a$, the sum of the infimum of $s$ and $a$ equals the infimum of the set obtained by adding $a$ to each element of $s$, i.e., \[ \inf s + a = \inf_{b \in s} (b + a). \]
ENNReal.add_iInf theorem
{a : ℝ≥0∞} : a + iInf f = ⨅ b, a + f b
Full source 
theorem add_iInf {a : ℝ≥0∞} : a + iInf f = ⨅ b, a + f b := by
  rw [add_comm, iInf_add]; simp [add_comm]
Addition of Constant Preserves Infimum in Extended Non-Negative Reals: $a + \bigsqcap_i f_i = \bigsqcap_i (a + f_i)$
Informal description
For any extended non-negative real number $a$ and any indexed family of extended non-negative real numbers $f : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$, the sum of $a$ and the infimum of $f$ equals the infimum of the family obtained by adding $a$ to each element of $f$, i.e., \[ a + \bigsqcap_{i} f_i = \bigsqcap_{i} (a + f_i). \]
ENNReal.iInf_add_iInf theorem
(h : ∀ i j, ∃ k, f k + g k ≤ f i + g j) : iInf f + iInf g = ⨅ a, f a + g a
Full source 
theorem iInf_add_iInf (h : ∀ i j, ∃ k, f k + g k ≤ f i + g j) : iInf f + iInf g = ⨅ a, f a + g a :=
  suffices ⨅ a, f a + g a ≤ iInf f + iInf g from
    le_antisymm (le_iInf fun _ => add_le_add (iInf_le _ _) (iInf_le _ _)) this
  calc
    ⨅ a, f a + g a ≤ ⨅ (a) (a'), f a + g a' :=
      le_iInf₂ fun a a' => let ⟨k, h⟩ := h a a'; iInf_le_of_le k h
    _ = iInf f + iInf g := by simp_rw [iInf_add, add_iInf]
Infimum Addition Law for Two Families in Extended Non-Negative Reals: $\bigsqcap_i f_i + \bigsqcap_j g_j = \bigsqcap_a (f_a + g_a)$ under Pairwise Dominance Condition
Informal description
For any indexed families of extended non-negative real numbers $f, g : \iota \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ satisfying the condition that for every $i, j$ there exists $k$ such that $f_k + g_k \leq f_i + g_j$, the sum of the infima of $f$ and $g$ equals the infimum of the pointwise sums, i.e., \[ \bigsqcap_i f_i + \bigsqcap_j g_j = \bigsqcap_a (f_a + g_a). \]
ENNReal.sup_eq_zero theorem
{a b : ℝ≥0∞} : a ⊔ b = 0 ↔ a = 0 ∧ b = 0
Full source 
theorem sup_eq_zero {a b : ℝ≥0∞} : a ⊔ ba ⊔ b = 0 ↔ a = 0 ∧ b = 0 :=
  sup_eq_bot_iff
Supremum Equals Zero in Extended Non-Negative Reals
Informal description
For any extended non-negative real numbers $a$ and $b$, the supremum $a \sqcup b$ equals $0$ if and only if both $a = 0$ and $b = 0$.
Mathlib.Meta.Positivity.evalENNRealOfReal definition
: PositivityExt
Full source 
/-- Extension for the `positivity` tactic: `ENNReal.ofReal`. -/
@[positivity ENNReal.ofReal _]
def evalENNRealOfReal : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℝ≥0∞), ~q(ENNReal.ofReal $a) =>
    let ra ← core q(inferInstance) q(inferInstance) a
    assertInstancesCommute
    match ra with
    | .positive pa => pure (.positive q(Iff.mpr (@ENNReal.ofReal_pos $a) $pa))
    | _ => pure .none
  | _, _, _ => throwError "not ENNReal.ofReal"
Positivity extension for `ENNReal.ofReal`
Informal description
The positivity extension tactic for `ENNReal.ofReal` checks whether the input real number is positive and, if so, proves that its image under `ENNReal.ofReal` is positive in the extended non-negative real numbers.