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∞.

Equations

• ENat.toENNReal = WithTop.map Nat.cast

instance ENat.hasCoeENNReal : CoeTC ℕ∞ ENNReal

Equations

• ENat.hasCoeENNReal = { coe := ENat.toENNReal }

@[simp]

theorem ENat.map_coe_nnreal : WithTop.map Nat.cast = ENat.toENNReal

def ENat.toENNRealOrderEmbedding : ℕ∞ ↪o ENNReal

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

Equations

• ENat.toENNRealOrderEmbedding = Nat.castOrderEmbedding.withTopMap

@[simp]

theorem ENat.toENNRealOrderEmbedding_apply : ⇑ENat.toENNRealOrderEmbedding = ENat.toENNReal

def ENat.toENNRealRingHom : ℕ∞ →+* ENNReal

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

Equations

• ENat.toENNRealRingHom = (Nat.castRingHom NNReal).withTopMap ENat.toENNRealRingHom.proof_1

@[simp]

theorem ENat.toENNRealRingHom_apply : ⇑ENat.toENNRealRingHom = ENat.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_coe_eq_iff {m n : ℕ∞} : ↑m = ↑n ↔ m = n

@[simp]

theorem ENat.toENNReal_le {m n : ℕ∞} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem ENat.toENNReal_lt {m n : ℕ∞} : ↑m < ↑n ↔ m < n

theorem ENat.toENNReal_mono : Monotone ENat.toENNReal

theorem ENat.toENNReal_strictMono : StrictMono ENat.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 : ℕ∞) : ↑(m ⊓ n) = ↑m ⊓ ↑n

@[simp]

theorem ENat.toENNReal_max (m n : ℕ∞) : ↑(m ⊔ n) = ↑m ⊔ ↑n

@[simp]

theorem ENat.toENNReal_sub (m n : ℕ∞) : ↑(m - n) = ↑m - ↑n