Documentation

Mathlib.Data.Real.ENatENNReal

Coercion from ℕ∞ to ℝ≥0∞ #

In this file we define a coercion from ℕ∞ to ℝ≥0∞ and prove some basic lemmas about this map.

Coercion from ℕ∞ to ℝ≥0∞.

Equations
Instances For

    Coercion ℕ∞ → ℝ≥0∞ as an OrderEmbedding.

    Equations
    Instances For

      Coercion ℕ∞ → ℝ≥0∞ as a ring homomorphism.

      Equations
      Instances For
        @[simp]
        @[simp]
        theorem ENat.toENNReal_coe (n : ) :
        n = n
        @[simp]
        theorem ENat.toENNReal_ofNat (n : ) [n.AtLeastTwo] :
        @[simp]
        theorem ENat.toENNReal_coe_eq_iff {m : ℕ∞} {n : ℕ∞} :
        m = n m = n
        @[simp]
        theorem ENat.toENNReal_le {m : ℕ∞} {n : ℕ∞} :
        m n m n
        @[simp]
        theorem ENat.toENNReal_lt {m : ℕ∞} {n : ℕ∞} :
        m < n m < n
        @[simp]
        theorem ENat.toENNReal_zero :
        0 = 0
        @[simp]
        theorem ENat.toENNReal_add (m : ℕ∞) (n : ℕ∞) :
        (m + n) = m + n
        @[simp]
        theorem ENat.toENNReal_one :
        1 = 1
        @[simp]
        theorem ENat.toENNReal_mul (m : ℕ∞) (n : ℕ∞) :
        (m * n) = m * n
        @[simp]
        theorem ENat.toENNReal_pow (x : ℕ∞) (n : ) :
        (x ^ n) = x ^ n
        @[simp]
        theorem ENat.toENNReal_min (m : ℕ∞) (n : ℕ∞) :
        (min m n) = min m n
        @[simp]
        theorem ENat.toENNReal_max (m : ℕ∞) (n : ℕ∞) :
        (max m n) = max m n
        @[simp]
        theorem ENat.toENNReal_sub (m : ℕ∞) (n : ℕ∞) :
        (m - n) = m - n