# 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
@[simp]

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_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_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