iff_le_add_mul — Mathlib

English

A map is Lipschitz on a set with constant K iff for all x,y in the set, f(x) ≤ f(y) + K d(x,y).

Русский

Функция Lipschitz на множестве с константой K эквивалентна неравенству f(x) ≤ f(y) + K d(x,y) для любых x,y на этом множестве.

LaTeX

$$$\\text{LipschitzOnWith}(K,f,s) \\iff \\forall x\\in s\\,\\forall y\\in s,\\ f(x) \\le f(y) + K \\cdot d(x,y)$$$

Lean4

protected theorem iff_le_add_mul {f : α → ℝ} {K : ℝ≥0} :
    LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y :=
  ⟨LipschitzOnWith.le_add_mul, LipschitzOnWith.of_le_add_mul K⟩

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