English
The Hausdorff dimension equals the supremum over all points x of the limsup of dimH over nhdsWithin x s.
Русский
Размерность Хаусдорфа равна супремуму по всем точкам x от лимпса dimH по nhdsWithin x s.
LaTeX
$$$$\\sup_{x} \\limsup\\dimH (\\mathcal{N}[s] x).smallSets = \\dimH s.$$$$
Lean4
/-- 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`. -/
theorem iSup_limsup_dimH (s : Set X) : ⨆ x, limsup dimH (𝓝[s] x).smallSets = dimH s :=
by
refine le_antisymm (iSup_le fun x => ?_) ?_
· refine limsup_le_of_le isCobounded_le_of_bot ?_
exact eventually_smallSets.2 ⟨s, self_mem_nhdsWithin, fun t => dimH_mono⟩
· rw [← bsupr_limsup_dimH]; exact iSup₂_le_iSup _ _
