toNNReal_smul — Mathlib

English

For r in NNReal and f in C(X, ℝ)₀, the action commutes with normalization: (r • f).toNNReal = r • f.toNNReal.

Русский

Для r в NNReal и f в C(X, ℝ)₀ выполняется: (r • f).toNNReal = r • f.toNNReal.

LaTeX

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

Lean4

@[simp]
theorem toNNReal_smul (r : ℝ≥0) (f : C(X, ℝ)₀) : (r • f).toNNReal = r • f.toNNReal :=
  by
  ext x
  by_cases h : 0 ≤ f x
  · simpa [max_eq_left h, NNReal.smul_def] using mul_nonneg r.coe_nonneg h
  · push_neg at h
    simpa [max_eq_right h.le, NNReal.smul_def] using mul_nonpos_of_nonneg_of_nonpos r.coe_nonneg h.le

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