toNNReal_algebraMap — Mathlib

English

The application of realification after composition equals the composition after applying toNNReal, i.e., real-continuous map composed with toNNReal equals toReal applied to the original map.

Русский

Применение преобразования к действительным после композиции равно композиции с применением toNNReal к исходной карте.

LaTeX

$$$\\phi^{\\mathrm{real}}( (\\mathrm{ContinuousMap.mk}\\; toReal\\; \\mathrm{continuous\\_coe}).\\circ f) = \\phi^{\\mathrm{real}}(f)$$$

Lean4

@[simp]
theorem toNNReal_algebraMap (r : ℝ≥0) : (algebraMap ℝ C(X, ℝ) r).toNNReal = algebraMap ℝ≥0 C(X, ℝ≥0) r := by ext; simp

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