range_normSq — Mathlib

English

The image of the squared-norm map is the nonnegative reals: range(normSq) = [0, ∞).

Русский

Образ отображения квадрата нормы равен неотрицательным вещественным числам: range(normSq) = [0, ∞).

LaTeX

$$$\\operatorname{range}(\\operatorname{normSq}) = [0, \\infty)$$$

Lean4

@[simp]
theorem range_normSq : range normSq = Ici 0 :=
  Subset.antisymm (range_subset_iff.2 normSq_nonneg) fun x hx => ⟨√x, by rw [normSq_ofReal, Real.mul_self_sqrt hx]⟩

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