mathlib3 documentation

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.

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

Equations
@[simp, norm_cast]
@[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 : ℕ∞) :
@[simp]
theorem enat.coe_ennreal_bit1 (n : ℕ∞) :
@[simp]
theorem enat.coe_ennreal_mul (m n : ℕ∞) :
(m * n) = m * n
@[simp]
theorem enat.coe_ennreal_sub (m n : ℕ∞) :
(m - n) = m - n