ediam_image_le_of_le — Mathlib

English

If hf is Hölder on s, then for any d, if dist(s) ≤ d in the ENNReal sense, then dist of images is bounded by C times d^r.

Русский

Пусть hf — Hölder на s; если расстояние множества ≤ d, то расстояние образов ≤ C d^r.

LaTeX

$$$\\text{HolderOnWith } C r f s \\Rightarrow \\forall d:\\mathrm{ENNReal}, \\mathrm{ediam}(t) ≤ d \\Rightarrow \\mathrm{ediam}(f''t) ≤ (C) * d^{r}$$$

Lean4

theorem ediam_image_le_of_le (hf : HolderOnWith C r f s) {d : ℝ≥0∞} (hd : EMetric.diam s ≤ d) :
    EMetric.diam (f '' s) ≤ (C : ℝ≥0∞) * d ^ (r : ℝ) :=
  EMetric.diam_image_le_iff.2 fun _ hx _ hy => hf.edist_le_of_le hx hy <| (EMetric.edist_le_diam_of_mem hx hy).trans hd

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