Theorems · Theorem · measure theory

bsupr_limsup_dimH

∀ {X : Type u_2} [inst : EMetricSpace X] [SecondCountableTopology X] (s : Set X),
  ⨆ x ∈ s, 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 x ∈ s of the limit superiors of dimH t along (𝓝[s] x).smallSets.

Defined in

Mathlib.Topology.MetricSpace.HausdorffDimension

Cited by

1 results in Mathlib

Foundations

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

Assumes

EMetricSpaceSecondCountableTopology