Coercion from ℕ∞ to ℝ≥0∞

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

def ENat.toENNReal : ℕ∞ → ENNReal

Coercion from ℕ∞ to ℝ≥0∞.

@[implicit_reducible]

instance ENat.hasCoeENNReal : CoeTC ℕ∞ ENNReal

@[simp]

theorem ENat.map_coe_nnreal : map Nat.cast = toENNReal

def ENat.toENNRealOrderEmbedding : ℕ∞ ↪o ENNReal

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

@[simp]

theorem ENat.toENNRealOrderEmbedding_apply : ⇑toENNRealOrderEmbedding = WithTop.map Nat.cast

noncomputable def ENat.toENNRealRingHom : ℕ∞ →+* ENNReal

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

@[simp]

theorem ENat.toENNRealRingHom_apply : ⇑toENNRealRingHom = toENNReal

@[simp]

theorem ENat.toENNReal_top : ↑⊤ = ⊤

@[simp]

theorem ENat.toENNReal_coe (n : ℕ) : ↑↑n = ↑n

@[simp]

theorem ENat.toENNReal_ofNat (n : ℕ) [n.AtLeastTwo] : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem ENat.toENNReal_inj {m n : ℕ∞} : ↑m = ↑n ↔ m = n

@[simp]

theorem ENat.toENNReal_eq_top {n : ℕ∞} : ↑n = ⊤ ↔ n = ⊤

theorem ENat.toENNReal_ne_top {n : ℕ∞} : ↑n ≠ ⊤ ↔ 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_lt_top {n : ℕ∞} : ↑n < ⊤ ↔ n < ⊤

theorem ENat.toENNReal_mono : Monotone toENNReal

theorem ENat.toENNReal_strictMono : StrictMono toENNReal

@[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