# mathlib3documentation

data.real.enat_ennreal

# Coercion from ℕ∞ to ℝ≥0∞#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
Equations
@[simp]
theorem enat.map_coe_nnreal  :
@[simp]

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

Equations
noncomputable def enat.to_ennreal_ring_hom  :

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

Equations
@[simp]
@[simp, norm_cast]
theorem enat.coe_ennreal_top  :
@[simp, norm_cast]
theorem enat.coe_ennreal_coe (n : ) :
@[simp, norm_cast]
theorem enat.coe_ennreal_le {m n : ℕ∞} :
m n m n
@[simp, norm_cast]
theorem enat.coe_ennreal_lt {m n : ℕ∞} :
m < n m < n
@[simp, norm_cast]
theorem enat.coe_ennreal_zero  :
0 = 0
@[simp]
theorem enat.coe_ennreal_add (m n : ℕ∞) :
(m + n) = m + n
@[simp]
theorem enat.coe_ennreal_one  :
1 = 1
@[simp]
theorem enat.coe_ennreal_bit0 (n : ℕ∞) :
(bit0 n) =
@[simp]
theorem enat.coe_ennreal_bit1 (n : ℕ∞) :
(bit1 n) =
@[simp]
theorem enat.coe_ennreal_mul (m n : ℕ∞) :
(m * n) = m * n
@[simp]
theorem enat.coe_ennreal_min (m n : ℕ∞) :
n) =
@[simp]
theorem enat.coe_ennreal_max (m n : ℕ∞) :
n) =
@[simp]
theorem enat.coe_ennreal_sub (m n : ℕ∞) :
(m - n) = m - n