toNNReal_neg_algebraMap — Mathlib

English

The negative of the algebra map to NNReal collapses to zero, i.e., (-algebraMap ℝ C(X,ℝ) r).toNNReal = 0 for any r ≥ 0.

Русский

Отрицание отображения алгебраического в NNReal обнуляет результат: (-algebraMap ℝ C(X, ℝ) r).toNNReal = 0.

LaTeX

$$$(-\\mathrm{algebraMap}_{\\mathbb{R}} C(X,\\mathbb{R})\\ r)^{\\toNNReal} = 0$$$

Lean4

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

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