lipschitzWith_one_nnnorm'

Mathlib.Analysis.Normed.Group.Uniform

URI: https://scilib.ai/kg/mathlib#lipschitzWith_one_nnnorm'

English

The NN-norm function is 1-Lipschitz: for all x,y, |‖x‖₊ − ‖y‖₊| ≤ ‖x−y‖.

Русский

NN-нормa функция является 1-липшицевой: для всех x,y верно |‖x‖₊ − ‖y‖₊| ≤ ‖x−y‖.

LaTeX

$$$|\|x\|_+ - \|y\|_+| \le \|x-y\|$$$

Lean4

@[to_additive lipschitzWith_one_nnnorm]
theorem lipschitzWith_one_nnnorm' : LipschitzWith 1 (NNNorm.nnnorm : E → ℝ≥0) :=
  lipschitzWith_one_norm'

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

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

Разделы

Аффилиация

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