range_nnnorm

Mathlib.Analysis.Normed.Module.RCLike.Real

URI: https://scilib.ai/kg/mathlib#range_nnnorm

English

In a nontrivial real normed space E, the range of nnnorm equals all of ℝ≥0.

Русский

В ненулевом вещественном нормированном пространстве E образ nnnorm покрывает всё ℝ≥0.

LaTeX

$$$$ \operatorname{range}(\text{nnnorm} : E \to \mathbb{R}_{\ge 0}) = \text{univ}. $$$$

Lean4

@[simp]
theorem range_nnnorm : range (nnnorm : E → ℝ≥0) = univ :=
  (nnnorm_surjective E).range_eq

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru