map_coe_nnreal — Mathlib

English

The map ENat.map commutes with the natural-number coercion: ENat.map ((↑) : ℕ → ℝ≥0) equals ((↑) : ℕ∞ → ℝ≥0∞).

Русский

Отображение ENat совместимо с включением натуральных чисел: ENat.map (↑) = (↑).

LaTeX

$$$ENat.map((\\uparrow):\\mathbb{N}\\to \\mathbb{R}_{\ge 0}) = (\\uparrow):\\mathbb{N}_{\\infty}\\to \\mathbb{R}_{\\ge 0,\\infty}$$$

Lean4

@[simp]
theorem map_coe_nnreal : ENat.map ((↑) : ℕ → ℝ≥0) = ((↑) : ℕ∞ → ℝ≥0∞) :=
  rfl

Похожие утверждения