nnrealPart — Mathlib

English

The nnrealPart map converts a bounded real-valued compactly supported function into a bounded NNReal-valued function by applying Real.toNNReal pointwise.

Русский

Функция nnrealPart переводит ограниченную вещественную компактно поддерживаемую функцию в ограниченную функцию значений ℝ≥0 путём применения Real.toNNReal по точкам.

LaTeX

$$$$ \mathrm{nnrealPart}(f) \;:\; x \mapsto \mathrm{Real.toNNReal}(f(x)). $$$$

Lean4

/-- The nonnegative part of a bounded continuous `ℝ`-valued function as a bounded
continuous `ℝ≥0`-valued function. -/
noncomputable def nnrealPart (f : C_c(α, ℝ)) : C_c(α, ℝ≥0)
    where
  toFun := Real.toNNReal.comp f.toFun
  continuous_toFun := Continuous.comp continuous_real_toNNReal f.continuous
  hasCompactSupport' := HasCompactSupport.comp_left f.hasCompactSupport' Real.toNNReal_zero

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