toReal — Mathlib

English

There is a canonical map that regards a compactly supported nonnegative real-valued function as a real-valued one by the natural inclusion ℝ≥0 ↪ ℝ.

Русский

Существует каноническое отображение, которое рассматривает компактно поддерживаемую неотрицательную функцию действительных значений как функцию действительных значений посредством естественного включения ℝ≥0 в ℝ.

LaTeX

$$$\\text{toReal}: C_c(\\alpha, \\mathbb{R}_{\\ge 0}) \\to C_c(\\alpha, \\mathbb{R}), \\quad f \\mapsto f$ (через естественную инклюзию $\\mathbb{R}_{\\ge 0} \\hookrightarrow \\mathbb{R}$).$$

Lean4

/-- The compactly supported continuous `ℝ≥0`-valued function as a compactly supported `ℝ`-valued
function. -/
noncomputable def toReal (f : C_c(α, ℝ≥0)) : C_c(α, ℝ) :=
  f.compLeft ContinuousMap.coeNNRealReal

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