normedField

Mathlib.Analysis.Normed.Field.Basic

URI: https://scilib.ai/kg/mathlib#Real.normedField

English

The real numbers form a normed field with norm given by the absolute value.

Русский

Действительные числа образуют нормированное поле с нормой, равной абсолютной величине.

LaTeX

$$$ \text{NormedField}(\mathbb{R}) \\text{ with } \|x\| = |x| $$$

Lean4

noncomputable instance normedField : NormedField ℝ :=
  { Real.normedAddCommGroup, Real.instField with norm_mul := abs_mul }

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

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

Разделы

Аффилиация

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