ofNNReal_natCast_sub

Mathlib.Data.ENNReal.Basic

URI: https://scilib.ai/kg/mathlib#ENNReal.ofNNReal_natCast_sub

English

For n ∈ Nat and r ∈ NNReal, ofNNReal (n - r) = n - r; the embedding commutes with subtraction.

Русский

Для n ∈ Nat и r ∈ NNReal: ofNNReal (n - r) = n - r; вложение сохраняет вычитание.

LaTeX

$$$$ \operatorname{ofNNReal} (n - r) = n - r. $$$$

Lean4

@[simp, norm_cast]
theorem ofNNReal_natCast_sub (n : ℕ) (r : ℝ≥0) : ofNNReal (n - r) = n - r :=
  rfl

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

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

Разделы

Аффилиация

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