ediam_image_le — Mathlib

English

The diameter of the image of a set under a Hölder function is controlled by the diameter of the set.

Русский

Диаметр образа множества под Холдер-функцией контролируется диаметром множества.

LaTeX

$$$\operatorname{diam}\big(f[A]\big) \le (C) \cdot \operatorname{diam}(A)^{r}$$$

Lean4

theorem ediam_image_le (hf : HolderWith C r f) (s : Set X) :
    EMetric.diam (f '' s) ≤ (C : ℝ≥0∞) * EMetric.diam s ^ (r : ℝ) :=
  EMetric.diam_image_le_iff.2 fun _ hx _ hy => hf.edist_le_of_le <| EMetric.edist_le_diam_of_mem hx hy

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