dist_le_of_le — Mathlib

English

For x,y in s, the distance after f is bounded by C times dist(x,y)^{r}.

Русский

Для x,y в s расстояние после применения f ограничено C · dist(x,y)^{r}.

LaTeX

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

Lean4

theorem dist_le_of_le (hf : HolderOnWith C r f s) (hx : x ∈ s) (hy : y ∈ s) {d : ℝ} (hd : dist x y ≤ d) :
    dist (f x) (f y) ≤ C * d ^ (r : ℝ) :=
  by
  lift d to ℝ≥0 using dist_nonneg.trans hd
  rw [dist_nndist] at hd ⊢
  norm_cast at hd ⊢
  exact hf.nndist_le_of_le hx hy hd

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