lipschitzWith_posPart — Mathlib

English

In a lattice-ordered normed group with a solid norm, the positive part map x ↦ x⁺ is 1-Lipschitz: ‖x⁺ − y⁺‖ ≤ ‖x − y‖ for all x, y.

Русский

В решётчатом нормированном группе с твёрдой нормой отображение положительной части x⁺ является 1‑липшицевым: ‖x⁺ − y⁺‖ ≤ ‖x − y‖ для любых x, y.

LaTeX

$$$\|x^{+} - y^{+}\| \le \|x - y\|$$$

Lean4

theorem lipschitzWith_posPart : LipschitzWith 1 (posPart : α → α) :=
  lipschitzWith_sup_right 0

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