nndist_le_of_le — Mathlib

English

If edist is controlled by a d, then the nndist after applying f is controlled by the corresponding bound.

Русский

Если edist(x,y) ≤ d, то nndist(fx,fy) ≤ C · d^{r}.

LaTeX

$$$\text{nndist}(f(x), f(y)) \le C \cdot d^{r}$ whenever $\text{edist}(x,y) ≤ d$$$

Lean4

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

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