dimH_range_le — Mathlib

English

If f is Lipschitz with coefficient K, then the Hausdorff dimension of its range is at most the dimension of its domain.

Русский

Если отображение f Lipschitz с коэффициентом K, то размерность Хаусдорфа образа не больше размерности домена.

LaTeX

$$$$\\dimH(\\operatorname{range} f) \\leq \\dimH(\\operatorname{univ}).$$$$

Lean4

/-- If `f` is a Lipschitz continuous map, then the Hausdorff dimension of its range is at most the
Hausdorff dimension of its domain. -/
theorem dimH_range_le (h : LipschitzWith K f) : dimH (range f) ≤ dimH (univ : Set X) :=
  @image_univ _ _ f ▸ h.dimH_image_le univ

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