English
If f is Lipschitz in a neighborhood of each point of s, then the dimension bound holds for the image of s.
Русский
Если f локально Lipschitz в окрестностях каждой точки множества s, то для образа s выполняется оценка размерности.
LaTeX
$$$$\\dimH(\\operatorname{image} f\\, s) \\leq \\dimH s.$$$$
Lean4
/-- If `s` is a set in an extended metric space `X` with second countable topology and `f : X → Y`
is Lipschitz in a neighborhood within `s` of every point `x ∈ s`, then the Hausdorff dimension of
the image `f '' s` is at most the Hausdorff dimension of `s`. -/
theorem dimH_image_le_of_locally_lipschitzOn [SecondCountableTopology X] {f : X → Y} {s : Set X}
(hf : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, LipschitzOnWith C f t) : dimH (f '' s) ≤ dimH s :=
by
have : ∀ x ∈ s, ∃ C : ℝ≥0, ∃ t ∈ 𝓝[s] x, HolderOnWith C 1 f t := by simpa only [holderOnWith_one] using hf
simpa only [ENNReal.coe_one, div_one] using dimH_image_le_of_locally_holder_on zero_lt_one this
