ofNNReal_natCast_add

Mathlib.Data.ENNReal.Basic

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

English

For r ∈ NNReal and n ∈ Nat, ofNNReal (n + r) = n + r; addition 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_natCast_add (n : ℕ) (r : ℝ≥0) : ofNNReal (n + r) = n + r :=
  rfl

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

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

Разделы

Аффилиация

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