nnnorm — Mathlib

English

The absolute value of a real-valued bounded continuous function is viewed as a bounded continuous function with nonnegative values, i.e., f ↦ |f| as α →ᵇ ℝ≥0, defined by (nnnorm f)(x) = |f(x)|.

Русский

Абсолютное значение вещественной ограниченно непрерывной функции трактуется как ограниченная непрерывная функция в ℝ≥0: (nnnorm f)(x) = |f(x)|.

LaTeX

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

Lean4

/-- The absolute value of a bounded continuous `ℝ`-valued function as a bounded
continuous `ℝ≥0`-valued function. -/
def nnnorm (f : α →ᵇ ℝ) : α →ᵇ ℝ≥0 :=
  BoundedContinuousFunction.comp _ (show LipschitzWith 1 fun x : ℝ => ‖x‖₊ from lipschitzWith_one_norm) f

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