Theorems · Theorem · measure theory

exists_mem_nhdsWithin_lt_dimH_of_lt_dimH

∀ {X : Type u_2} [inst : EMetricSpace X] [SecondCountableTopology X] {s : Set X} {r : ENNReal},
  r < dimH s → ∃ x ∈ s, ∀ t ∈ nhdsWithin x s, r < dimH t

If r is less than the Hausdorff dimension of a set s in an (extended) metric space with second countable topology, then there exists a point x ∈ s such that every neighborhood t of x within s has Hausdorff dimension greater than r.

Defined in

Mathlib.Topology.MetricSpace.HausdorffDimension

Cited by

1 results in Mathlib

Foundations

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

Assumes

EMetricSpaceSecondCountableTopology