Theorems · Theorem · measure theory

dimH_image_le_of_locally_lipschitzOn

∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [SecondCountableTopology X]
  {f : X → Y} {s : Set X}, (∀ x ∈ s, ∃ C, ∃ t ∈ nhdsWithin x s, LipschitzOnWith C f t) → dimH (f '' s) ≤ dimH s

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.

Defined in

Mathlib.Topology.MetricSpace.HausdorffDimension

Cited by

2 results in Mathlib

Foundations

Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EMetricSpaceEMetricSpaceSecondCountableTopology