lipschitzWith_sub — Mathlib

English

The Lipschitz condition for subtraction holds in a seminormed add-commutative group with NNReal bounds.

Русский

Условие липшицевости для вычитания выполняется в полугруппе с нормой с NNReal ограничениями.

LaTeX

$$$\text{lipschitzWith sub} :\; LipschitzWith\ 2\ (p\mapsto p.1-p.2)$$$

Lean4

theorem lipschitzWith_sub : LipschitzWith 2 (fun (p : R × R) ↦ p.1 - p.2) :=
  by
  convert LipschitzWith.prod_fst.sub LipschitzWith.prod_snd
  norm_num

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