edist_le — Mathlib

English

Let f be Hölder with constants C and r. Then for any x,y, the extended distance after applying f is controlled by the Hölder bound.

Русский

Пусть f удовлетворяет условию Холдер с константами C и r. Тогда для любых x,y после применения f расстояние под контролем Холдер-ограничения.

LaTeX

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

Lean4

theorem edist_le (h : HolderWith C r f) (x y : X) : edist (f x) (f y) ≤ (C : ℝ≥0∞) * edist x y ^ (r : ℝ) :=
  h x y

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