lipschitzWith_one_norm' — Mathlib

English

The norm function is 1-Lipschitz: it is Lipschitz with constant 1 with respect to the metric induced by the norm.

Русский

Функция нормы является 1-липшицевой: она имеет предел липшица с константой 1 относительно метрики, порождённой нормой.

LaTeX

$$$\text{LipschitzWith}(1, \|\cdot\|)$ or equivalently, $|\|x\| - \|y\| | \le \|x-y\|.$$$

Lean4

@[to_additive lipschitzWith_one_norm]
theorem lipschitzWith_one_norm' : LipschitzWith 1 (norm : E → ℝ) := by simpa using LipschitzWith.dist_right (1 : E)

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