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
                @[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 : ℕ∞) :
                ↑(min m n) = min ↑m ↑n
                source
                @[simp]
                theorem ENat.toENNReal_max (m n : ℕ∞) :
                ↑(max m n) = max ↑m ↑n
                source
                @[simp]
                theorem ENat.toENNReal_sub (m n : ℕ∞) :
                ↑(m - n) = ↑m - ↑n