nnnorm_eq — Mathlib

English

The NNReal norm agrees with the real norm: the real norm of x in ℝ≥0 equals x itself when viewed as a real number.

Русский

Норма для NNReal совпадает с вещественной нормой: норма в ℝ≥0, взятая как вещественное число, равна самому x.

LaTeX

$$$\| x : \mathbb{R} \| = x \quad \text{ for } x \ge 0$$$

Lean4

@[simp]
theorem nnnorm_eq (x : ℝ≥0) : ‖(x : ℝ)‖₊ = x := by ext; simp [nnnorm]

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