nnnorm_two

Mathlib.Analysis.Normed.Group.Basic

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

English

The NNReal norm of 2 (as a real) is 2.

Русский

NNReal-норма числа 2 как вещественного равна 2.

LaTeX

$$$$\|2\|_{+} = 2.$$$$

Lean4

theorem nnnorm_two : ‖(2 : ℝ)‖₊ = 2 :=
  NNReal.eq <| by simp

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

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

Разделы

Аффилиация

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