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⟩