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.

source
def ENat.toENNReal :
ℕ∞ → ENNReal

Coercion from ℕ∞ to ℝ≥0∞.

Equations
Instances For
    source
    instance ENat.hasCoeENNReal :
    CoeTC ℕ∞ ENNReal
    Equations
    source
    @[simp]
    theorem ENat.map_coe_nnreal :
    map Nat.cast = toENNReal
    source
    def ENat.toENNRealOrderEmbedding :
    ℕ∞ ↪o ENNReal

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

    Equations
    Instances For
      source
      @[simp]
      theorem ENat.toENNRealOrderEmbedding_apply :
      ⇑toENNRealOrderEmbedding = WithTop.map Nat.cast
      source
      def ENat.toENNRealRingHom :
      ℕ∞ →+* ENNReal

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

      Equations
      Instances For
        source
        @[simp]
        theorem ENat.toENNRealRingHom_apply :
        ⇑toENNRealRingHom = toENNReal
        source
        @[simp]
        theorem ENat.toENNReal_top :
        ↑⊤ = ⊤
        source
        @[simp]
        theorem ENat.toENNReal_coe (n : ℕ) :
        ↑↑n = ↑n
        source
        @[simp]
        theorem ENat.toENNReal_ofNat (n : ℕ) [n.AtLeastTwo] :
        ↑(OfNat.ofNat n) = OfNat.ofNat n
        source
        @[simp]
        theorem ENat.toENNReal_inj {m n : ℕ∞} :
        ↑m = ↑n ↔ m = n
        source
        @[deprecated ENat.toENNReal_inj (since := "2024-12-29")]
        theorem ENat.toENNReal_coe_eq_iff {m n : ℕ∞} :
        ↑m = ↑n ↔ m = n

        Alias of ENat.toENNReal_inj.

        source
        @[simp]
        theorem ENat.toENNReal_eq_top {n : ℕ∞} :
        ↑n = ⊤ ↔ n = ⊤
        source
        theorem ENat.toENNReal_ne_top {n : ℕ∞} :
        ↑n ≠ ⊤ ↔ n ≠ ⊤
        source
        @[simp]
        theorem ENat.toENNReal_le {m n : ℕ∞} :
        ↑m ≤ ↑n ↔ m ≤ n
        source
        @[simp]
        theorem ENat.toENNReal_lt {m n : ℕ∞} :
        ↑m < ↑n ↔ m < n
        source
        @[simp]
        theorem ENat.toENNReal_lt_top {n : ℕ∞} :
        ↑n < ⊤ ↔ n < ⊤
        source
        theorem ENat.toENNReal_mono :
        Monotone toENNReal
        source
        theorem ENat.toENNReal_strictMono :
        StrictMono toENNReal
        source
        @[simp]
        theorem ENat.toENNReal_zero :
        ↑0 = 0
        source
        @[simp]
        theorem ENat.toENNReal_add (m n : ℕ∞) :
        ↑(m + n) = ↑m + ↑n
        source
        @[simp]
        theorem ENat.toENNReal_one :
        ↑1 = 1
        source
        @[simp]
        theorem ENat.toENNReal_mul (m n : ℕ∞) :
        ↑(m * n) = ↑m * ↑n
        source
        @[simp]
        theorem ENat.toENNReal_pow (x : ℕ∞) (n : ℕ) :
        ↑(x ^ n) = ↑x ^ n
        source
        @[simp]
        theorem ENat.toENNReal_min (m n : ℕ∞) :
        ↑(m ⊓ n) = ↑m ⊓ ↑n
        source
        @[simp]
        theorem ENat.toENNReal_max (m n : ℕ∞) :
        ↑(m ⊔ n) = ↑m ⊔ ↑n
        source
        @[simp]
        theorem ENat.toENNReal_sub (m n : ℕ∞) :
        ↑(m - n) = ↑m - ↑n