toNNReal — Mathlib

English

The construction toNNReal sends a continuous map f : C(X, ℝ)₀ to a continuous map f.toNNReal : C(X, ℝ≥0)₀, and this assignment is continuous as a map between the function spaces endowed with the appropriate topology.

Русский

Построение toNNReal переводит непрерывную функцию f : C(X, ℝ)₀ в непрерывную функцию f.toNNReal : C(X, ℝ≥0)₀, и это отображение непрерывно относительно соответствующей топологии пространств функций.

LaTeX

$$$toNNReal: C(X, \\mathbb{R})_{0} \\to C(X, \\mathbb{R}_{\\ge 0})_{0}$ непрерывно.$$

Lean4

/-- This map sends `f : C(X, ℝ)` to `Real.toNNReal ∘ f`, bundled as a continuous map `C(X, ℝ≥0)`. -/
noncomputable def toNNReal (f : C(X, ℝ)₀) : C(X, ℝ≥0)₀ :=
  ⟨.realToNNReal |>.comp f, by simp⟩

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