projIcc — Mathlib

English

If a function f satisfies a distance bound f(x)≤f(y)+K·d(x,y) for all x,y∈s, then f is Lipschitz on s with constant Real.toNNReal(K).

Русский

Если для всех x,y∈s справедливо f(x)≤f(y)+K·d(x,y), тогда f — Lipschitz на s с константой Real.toNNReal(K).

LaTeX

$$$\\forall x,y\\in s,\\; f(x) \\le f(y) + K \\cdot d(x,y) \\Rightarrow \\operatorname{LipschitzOnWith}(\\operatorname{Real.toNNReal}(K), f, s)$$$

Lean4

protected theorem projIcc {a b : ℝ} (h : a ≤ b) : LipschitzWith 1 (projIcc a b h) :=
  ((LipschitzWith.id.const_min _).const_max _).subtype_mk _

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