toNNReal_apply — Mathlib

English

On applying toNNReal to a real-valued continuous map f, the value at a point x is the NNReal version of f(x): f.toNNReal(x) = Real.toNNReal(f(x)).

Русский

При применении toNNReal к непрерывной функции с вещественными значениями, значение в точке x равно NNReal-обратному от f(x): f.toNNReal(x) = Real.toNNReal(f(x)).

LaTeX

$$$f: C(X, \\mathbb{R})_{0},\\; x \\in X:\\quad (f.toNNReal)(x) = \\mathrm{Real.toNNReal}(f(x)).$$$

Lean4

@[simp]
theorem toNNReal_apply (f : C(X, ℝ)₀) (x : X) : f.toNNReal x = Real.toNNReal (f x) :=
  rfl

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