toNNReal_neg_smul — Mathlib

English

Negating a scaled function and then applying toNNReal equals scaling the toNNReal of the function by the same NNReal factor after negation.

Русский

Отрицание масштаба функции и применение toNNReal равны масштабированию toNNReal от функции после отрицания.

LaTeX

$$$toNNReal(-(r \\cdot f)) = r \\cdot (-f).toNNReal$$$

Lean4

@[simp]
theorem toNNReal_neg_smul (r : ℝ≥0) (f : C(X, ℝ)₀) : (-(r • f)).toNNReal = r • (-f).toNNReal := by
  rw [NNReal.smul_def, ← smul_neg, ← NNReal.smul_def, toNNReal_smul]

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