dist_le_of_le — Mathlib

English

For HolderOnWith, the real distance between f(x) and f(y) is bounded by the Hölder bound with respect to dist x y.

Русский

Для HolderOnWith расстояние между f(x) и f(y) ограничено Холдер-ограничением по dist(x,y).

LaTeX

$$$\operatorname{dist}(f(x), f(y)) \le C \cdot (\operatorname{dist}(x,y))^{r}$$$

Lean4

theorem dist_le_of_le (hf : HolderWith C r f) {x y : X} {d : ℝ} (hd : dist x y ≤ d) :
    dist (f x) (f y) ≤ C * d ^ (r : ℝ) :=
  (hf.holderOnWith univ).dist_le_of_le (mem_univ x) (mem_univ y) hd

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