of_dist_le' — Mathlib

English

If f is Lipschitz on s with K, and f(x)−f(y)≤K·d(x,y) for all x,y∈s, then LipschitzOnWith K f s holds.

Русский

Если f липшицева на s с константой K и для всех x,y∈s выполняется f(x)−f(y)≤K·d(x,y), то LipschitzOnWith K f s верно.

LaTeX

$$$\\text{If } \\forall x,y\\in s:\\; f(x) \\le f(y) + K \\cdot d(x,y) \\Rightarrow \\operatorname{LipschitzOnWith}(K,f,s)$$$

Lean4

protected theorem of_dist_le' {K : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y) :
    LipschitzOnWith (Real.toNNReal K) f s :=
  of_dist_le_mul fun x hx y hy => le_trans (h x hx y hy) <| by gcongr; apply Real.le_coe_toNNReal

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