range_norm — Mathlib

English

Let E be a nontrivial real normed space. The set of all values of ‖x‖ as x ranges over E is exactly [0, ∞).

Русский

Пусть E — ненулевое вещественное нормированное пространство. Множество значений ‖x‖ при x ∈ E равно [0, ∞).

LaTeX

$$$$ \operatorname{range}(\|\cdot\|) = [0, \infty). $$$$

Lean4

@[simp]
theorem range_norm : range (norm : E → ℝ) = Ici 0 :=
  Subset.antisymm (range_subset_iff.2 norm_nonneg) fun _ => exists_norm_eq E

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