dimH_image_le — Mathlib

English

Same as above: if f is Lipschitz on a neighborhood of s, then dimH (f'' s) ≤ dimH s.

Русский

То же самое: если f локально Lipschitz на s, то dimH образа f(s) не больше dimH s.

LaTeX

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

Lean4

/-- If `f` is a Lipschitz continuous map, then `dimH (f '' s) ≤ dimH s`. -/
theorem dimH_image_le (h : LipschitzWith K f) (s : Set X) : dimH (f '' s) ≤ dimH s :=
  h.lipschitzOnWith.dimH_image_le

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