toENNReal_sub

Mathlib.Data.Real.ENatENNReal

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

English

The embedding preserves subtraction: image of m−n equals the subtraction of images.

Русский

Встраивание сохраняет вычитание: образ m−n равен разности образов.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem toENNReal_sub (m n : ℕ∞) : ↑(m - n) = (m - n : ℝ≥0∞) :=
  WithTop.map_sub Nat.cast_tsub Nat.cast_zero m n

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

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

Разделы

Аффилиация

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