nnnorm_surjective — Mathlib

English

In a nontrivial real normed space E, the map x ↦ nnnorm x from E to ℝ≥0 is surjective.

Русский

В ненулевом вещественном нормированном пространстве E отображение x ↦ nnnorm x из E в ℝ≥0 собирает всё множество значений (существует для каждого элемента ℝ≥0).

LaTeX

$$$$ \forall a \in \mathbb{R}_{\ge 0}, \exists x \in E \; \text{such that } \text{nnnorm}(x) = a. $$$$

Lean4

theorem nnnorm_surjective : Surjective (nnnorm : E → ℝ≥0) := fun c =>
  (exists_norm_eq E c.coe_nonneg).imp fun _ h => NNReal.eq h

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