range_norm — Mathlib

English

The set of all norms of complex numbers is exactly the nonnegative real numbers: range of the norm is [0, ∞).

Русский

Множество значений нормы всех комплексных чисел равно неотрицательным вещественным числам: диапазон нормы — [0, ∞).

LaTeX

$$$\\operatorname{range}(\\|\\cdot\\| : \\mathbb{C} \\to \\mathbb{R}) = [0, \\infty)$$$

Lean4

@[simp 1100]
protected theorem range_norm : range (‖·‖ : ℂ → ℝ) = Set.Ici 0 :=
  Subset.antisymm (range_subset_iff.2 norm_nonneg) fun x hx ↦ ⟨x, Complex.norm_of_nonneg hx⟩

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