iff_le_add_mul — Mathlib

English

The equivalence of LipschitzWith with a pointwise distance inequality for real-valued f.

Русский

Эквивалентность LipschitzWith через неравенство расстояния для действительной функции.

LaTeX

$$$\text{LipschitzWith } K f \iff \forall x,y, f(x) \le f(y) + K \cdot \operatorname{dist}(x,y)$$$

Lean4

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

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