norm_of_nonneg

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.norm_of_nonneg

English

If r is a nonnegative real number, then the norm of its image in K equals r.

Русский

Если r неотрицательно, то нормa образа r в K равна r.

LaTeX

$$$$0 \le r \implies \| (r : K) \| = r.$$$$

Lean4

theorem norm_of_nonneg {r : ℝ} (h : 0 ≤ r) : ‖(r : K)‖ = r :=
  (norm_ofReal _).trans (abs_of_nonneg h)

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

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

Разделы

Аффилиация

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