toENNReal_add

Mathlib.Data.Real.ENatENNReal

URI: https://scilib.ai/kg/mathlib#ENat.toENNReal_add

English

The embedding preserves addition: the image of m+n equals the sum of the images.

Русский

Встраивание сохраняет сложение: образ суммы равен сумме образов.

LaTeX

$$$\\uparrow (m+n) = (m+n) \\text{ in } \\mathbb{R}_{\\ge 0,\\infty}.$$$

Lean4

@[simp, norm_cast]
theorem toENNReal_add (m n : ℕ∞) : ↑(m + n) = (m + n : ℝ≥0∞) :=
  map_add toENNRealRingHom m n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru