dimH_image — Mathlib

English

If f is an isometry, then the Hausdorff dimension of the image of a set equals the Hausdorff dimension of the set.

Русский

Если отображение является изометрией, то размерность Хаусдорфа образа множества равна размерности самого множества.

LaTeX

$$$$\\dimH( f'' s) = \\dimH s.$$$$

Lean4

theorem dimH_image (hf : Isometry f) (s : Set X) : dimH (f '' s) = dimH s :=
  le_antisymm (hf.lipschitz.dimH_image_le _) (hf.antilipschitz.le_dimH_image _)

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