Theorems · Theorem · measure theory

iSup_limsup_dimH

∀ {X : Type u_2} [inst : EMetricSpace X] [SecondCountableTopology X] (s : Set X),
  ⨆ x, Filter.limsup dimH (nhdsWithin x s).smallSets = dimH s

In an (extended) metric space with second countable topology, the Hausdorff dimension of a set s is the supremum over all x of the limit superiors of dimH t along (𝓝[s] x).smallSets.

Defined in

Mathlib.Topology.MetricSpace.HausdorffDimension

Cited by

0 results in Mathlib

Foundations

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

Assumes

EMetricSpaceSecondCountableTopology