dimH_image_le — Mathlib

English

If s is a set on which f is Lipschitz in neighborhoods, then dimH (f'' s) ≤ dimH s.

Русский

Если на множестве s функция f локально Lipschitz, то dimH образа f(s) не превосходит dimH s.

LaTeX

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

Lean4

/-- If `f : X → Y` is Lipschitz continuous on `s`, then `dimH (f '' s) ≤ dimH s`. -/
theorem dimH_image_le (h : LipschitzOnWith K f s) : dimH (f '' s) ≤ dimH s := by
  simpa using h.holderOnWith.dimH_image_le zero_lt_one

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