English
If r is less than the Hausdorff dimension of s, then there exists a point x in s such that every nhdsWithin x in s has dimH greater than r.
Русский
Если r менее чем размерность Хаусдорфа множества s, то существует точка x ∈ s, для которой каждый окрестность nhdsWithin x внутри s имеет dimH большее чем r.
LaTeX
$$$$\\exists x \\in s, \\forall t \\in \\mathcal{N}_s(x),\\ r < \\dimH t.$$$$
Lean4
/-- 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`. -/
theorem exists_mem_nhdsWithin_lt_dimH_of_lt_dimH {s : Set X} {r : ℝ≥0∞} (h : r < dimH s) :
∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t := by
contrapose! h; choose! t htx htr using h
rcases countable_cover_nhdsWithin htx with ⟨S, hSs, hSc, hSU⟩
calc
dimH s ≤ dimH (⋃ x ∈ S, t x) := dimH_mono hSU
_ = ⨆ x ∈ S, dimH (t x) := (dimH_bUnion hSc _)
_ ≤ r := iSup₂_le fun x hx => htr x <| hSs hx
