English
If f is Lipschitz in a neighborhood of every point of s in a space with second countable topology, then dimH (f'' s) ≤ dimH s.
Русский
Если f локально Lipschitz в окрестностях каждой точки s в пространстве с двойной счётностью, то dimH образа f(s) ≤ dimH s.
LaTeX
$$$$\\dimH(\\operatorname{image} f\\, s) \\leq \\dimH s.$$$$
Lean4
/-- If `f : X → Y` is Lipschitz in a neighborhood of each point `x : X`, then the Hausdorff
dimension of `range f` is at most the Hausdorff dimension of `X`. -/
theorem dimH_range_le_of_locally_lipschitzOn [SecondCountableTopology X] {f : X → Y}
(hf : ∀ x : X, ∃ C : ℝ≥0, ∃ s ∈ 𝓝 x, LipschitzOnWith C f s) : dimH (range f) ≤ dimH (univ : Set X) :=
by
rw [← image_univ]
refine dimH_image_le_of_locally_lipschitzOn fun x _ => ?_
simpa only [exists_prop, nhdsWithin_univ] using hf x