dimH_image_le — Mathlib

English

If f is HölderWith with exponent r on domain X, then dimH(image f s) ≤ dimH s / r for any set s.

Русский

Если f — HölderWith с экспонентой r на домене X, то dimH образа f(s) не превышает dimH s / r для любого множества s.

LaTeX

$$$$\\dimH(\\operatorname{image} f\, s) \\leq \\frac{\\dimH s}{r}.$$$$

Lean4

/-- If `f : X → Y` is Hölder continuous with a positive exponent `r`, then the Hausdorff dimension
of the image of a set `s` is at most `dimH s / r`. -/
theorem dimH_image_le (h : HolderWith C r f) (hr : 0 < r) (s : Set X) : dimH (f '' s) ≤ dimH s / r :=
  (h.holderOnWith s).dimH_image_le hr

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