lipschitzWith_negPart — Mathlib

English

Similarly, the negative part map x ↦ x⁻ is 1-Lipschitz in a lattice-ordered normed group with a solid norm: ‖x⁻ − y⁻‖ ≤ ‖x − y‖ for all x, y.

Русский

Аналогично отображение отрицательной части x⁻ является 1‑липшицевым: ‖x⁻ − y⁻‖ ≤ ‖x − y‖.

LaTeX

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

Lean4

theorem lipschitzWith_negPart : LipschitzWith 1 (negPart : α → α) := by
  simpa [Function.comp] using lipschitzWith_posPart.comp LipschitzWith.id.neg

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