le_dimH_image — Mathlib

English

For any Lipschitz-like mapping, the preimage dimension bound implies the image dimension bound, i.e., dimH s ≤ dimH (f'' s).

Русский

Для любого отображения со свойством схожим с липшицевостью, граница размерности предобраза дает границу образа: dimH s ≤ dimH (f'' s).

LaTeX

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

Lean4

theorem le_dimH_image (hf : AntilipschitzWith K f) (s : Set X) : dimH s ≤ dimH (f '' s) :=
  calc
    dimH s ≤ dimH (f ⁻¹' (f '' s)) := dimH_mono (subset_preimage_image _ _)
    _ ≤ dimH (f '' s) := hf.dimH_preimage_le _

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