Theorems · Theorem · measure theory

HolderOnWith.dimH_image_le

∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X}, HolderOnWith C r f s → 0 < r → dimH (f '' s) ≤ dimH s / ↑r

If f is a Hölder continuous map with exponent r > 0, then dimH (f '' s) ≤ dimH s / r.

Defined in

Mathlib.Topology.MetricSpace.HausdorffDimension

Cited by

3 results in Mathlib

Foundations

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

Assumes

EMetricSpaceEMetricSpace