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.

source
@[protected, instance]
def enat.has_coe_ennreal  :
has_coe_t ℕ∞ ennreal
Equations
source
@[simp]
theorem enat.map_coe_nnreal  :
with_top.map coe = coe
source
@[simp]
theorem enat.to_ennreal_order_embedding_apply  :
⇑enat.to_ennreal_order_embedding = coe
source
def enat.to_ennreal_order_embedding  :
ℕ∞ ↪o ennreal

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

Equations
source
noncomputable def enat.to_ennreal_ring_hom  :
ℕ∞ →+* ennreal

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

Equations
source
@[simp]
theorem enat.to_ennreal_ring_hom_apply  :
⇑enat.to_ennreal_ring_hom = coe
source
@[simp, norm_cast]
theorem enat.coe_ennreal_top  :
↑⊤ = ⊤
source
@[simp, norm_cast]
theorem enat.coe_ennreal_coe (n : ℕ) :
↑↑n = ↑n
source
@[simp, norm_cast]
theorem enat.coe_ennreal_le {m n : ℕ∞} :
↑m ≤ ↑n ↔ m ≤ n
source
@[simp, norm_cast]
theorem enat.coe_ennreal_lt {m n : ℕ∞} :
↑m < ↑n ↔ m < n
source
theorem enat.coe_ennreal_mono  :
monotone coe
source
theorem enat.coe_ennreal_strict_mono  :
strict_mono coe
source
@[simp, norm_cast]
theorem enat.coe_ennreal_zero  :
↑0 = 0
source
@[simp]
theorem enat.coe_ennreal_add (m n : ℕ∞) :
↑(m + n) = ↑m + ↑n
source
@[simp]
theorem enat.coe_ennreal_one  :
↑1 = 1
source
@[simp]
theorem enat.coe_ennreal_bit0 (n : ℕ∞) :
↑(bit0 n) = bit0 ↑n
source
@[simp]
theorem enat.coe_ennreal_bit1 (n : ℕ∞) :
↑(bit1 n) = bit1 ↑n
source
@[simp]
theorem enat.coe_ennreal_mul (m n : ℕ∞) :
↑(m * n) = ↑m * ↑n
source
@[simp]
theorem enat.coe_ennreal_min (m n : ℕ∞) :
↑(linear_order.min m n) = linear_order.min ↑m ↑n
source
@[simp]
theorem enat.coe_ennreal_max (m n : ℕ∞) :
↑(linear_order.max m n) = linear_order.max ↑m ↑n
source
@[simp]
theorem enat.coe_ennreal_sub (m n : ℕ∞) :
↑(m - n) = ↑m - ↑n