ofNNReal_sub_natCast

Mathlib.Data.ENNReal.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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