nnrealPart — Mathlib

English

For f: α →ᵇ ℝ, the nnreal part maps f to a bounded continuous function α →ᵇ ℝ≥0 by applying the nonnegative part at each point, i.e., (nnrealPart f)(x) = max{f(x), 0} in ℝ≥0.

Русский

Положительная часть функции f применяется по точкам, получая функцию в ℝ≥0: (nnrealPart f)(x) = max{f(x),0}.

LaTeX

$$$\forall f:\, \alpha \to^b \mathbb{R},\; (\text{nnrealPart } f)(x) = \max\{f(x),0\}\text{ in } \mathbb{R}_{\ge 0}. $$$$

Lean4

/-- The nonnegative part of a bounded continuous `ℝ`-valued function as a bounded
continuous `ℝ≥0`-valued function. -/
def nnrealPart (f : α →ᵇ ℝ) : α →ᵇ ℝ≥0 :=
  BoundedContinuousFunction.comp _ (show LipschitzWith 1 Real.toNNReal from lipschitzWith_posPart) f

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