posPart_algebraMap_nnreal — Mathlib

English

For r in NNReal, the positive part of the natural-algebra map coincides with the map of r: (algebraMap ℝ≥0 A r)⁺ = algebraMap ℝ≥0 A r.

Русский

Для r в NNReal положительная часть образа алгебра maps совпадает с образом r: (algebraMap ℝ≥0 A r)⁺ = algebraMap ℝ≥0 A r.

LaTeX

$$$( algebraMap \\mathbb{R}_{\\ge 0} A \\; r )^+ = algebraMap \\mathbb{R}_{\\ge 0} A \\; r$$$

Lean4

@[simp]
theorem posPart_algebraMap_nnreal (r : ℝ≥0) : (algebraMap ℝ≥0 A r)⁺ = algebraMap ℝ≥0 A r :=
  by
  rw [CFC.posPart_def, cfcₙ_eq_cfc, IsScalarTower.algebraMap_apply ℝ≥0 ℝ A]
  simp

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