Theorems · Theorem · measure theory

dimH_le

∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {s : Set X} {d : ENNReal},
  (∀ (d' : NNReal), (MeasureTheory.Measure.hausdorffMeasure ↑d') s = ⊤ → ↑d' ≤ d) → dimH s ≤ d

Defined in

Mathlib.Topology.MetricSpace.HausdorffDimension

Cited by

4 results in Mathlib

Foundations

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

Assumes

EMetricSpaceMeasurableSpaceBorelSpace