le_add_mul — Mathlib

English

If h is LipschitzOnWith on s, then f x ≤ f y + K d(x,y) for all x, y in s.

Русский

Если h — LipschitzOnWith на s, то f(x) ≤ f(y) + K d(x,y) для всех x,y в s.

LaTeX

$$$\\text{le\_add\_mul}: h \\Rightarrow \\forall x\\in s,\\forall y\\in s,\\; f(x) \\le f(y) + K \\cdot d(x,y)$$$

Lean4

protected theorem le_add_mul {f : α → ℝ} {K : ℝ≥0} (h : LipschitzOnWith K f s) {x : α} (hx : x ∈ s) {y : α}
    (hy : y ∈ s) : f x ≤ f y + K * dist x y :=
  sub_le_iff_le_add'.1 <| le_trans (le_abs_self _) <| h.dist_le_mul x hx y hy

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