English
If f is antilipschitz with constant K, then the Hausdorff dimension of the preimage of any set is at most the dimension of the set.
Русский
Если отображение антипилешиц с константой K, то размерность Хаусдорфа предобраза любого множества не больше размерности самого множества.
LaTeX
$$$$\\dimH(f^{-1}(s)) \\leq \\dimH(s).$$$$
Lean4
theorem dimH_preimage_le (hf : AntilipschitzWith K f) (s : Set Y) : dimH (f ⁻¹' s) ≤ dimH s :=
by
borelize X Y
refine dimH_le fun d hd => le_dimH_of_hausdorffMeasure_eq_top ?_
have := hf.hausdorffMeasure_preimage_le d.coe_nonneg s
rw [hd, top_le_iff] at this
contrapose! this
exact ENNReal.mul_ne_top (by simp) this