dimH_range_le_of_locally_lipschitzOn

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

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