ediam_image_inter_le — Mathlib

English

Let f be Hölder on a set s with constants C and r. Then for every subset t, the diameter of the image of t ∩ s under f is bounded by C times the diameter of t to the r-th power.

Русский

Пусть f удовлетворяет условию Холдер на множество s с константами C и r. Тогда для любого множества t диаметр образа f(t ∩ s) не превосходит C · diam(t)^{r}.

LaTeX

$$$\operatorname{diam}\big(f\big( t \cap s \big)\big) \le C \cdot \operatorname{diam}(t)^{r}$$$

Lean4

theorem ediam_image_inter_le (hf : HolderOnWith C r f s) (t : Set X) :
    EMetric.diam (f '' (t ∩ s)) ≤ (C : ℝ≥0∞) * EMetric.diam t ^ (r : ℝ) :=
  hf.ediam_image_inter_le_of_le le_rfl

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