norm_of_nonpos

Mathlib.Analysis.Normed.Group.Basic

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

English

If r ≤ 0, then ‖r‖ = -r.

Русский

Если r ≤ 0, тогда ‖r‖ = -r.

LaTeX

$$$\\text{(r \\le 0)} \\Rightarrow \\|r\\|_\\varepsilon = -r$$$

Lean4

theorem norm_of_nonpos (hr : r ≤ 0) : ‖r‖ = -r :=
  abs_of_nonpos hr

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

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

Разделы

Аффилиация

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