English
If s is a subset with a neighborhood of x, then dim_H(s) equals the dimension of the ambient space E.
Русский
Если множество s имеет окрестность в точке x, то dim_H(s) = dim_E.
LaTeX
$$$\\dim_H(s) = \\mathrm{finrank}_{\\mathbb{R}}(E)$$$
Lean4
theorem dimH_of_mem_nhds {x : E} {s : Set E} (h : s ∈ 𝓝 x) : dimH s = finrank ℝ E :=
by
have e : E ≃L[ℝ] Fin (finrank ℝ E) → ℝ := ContinuousLinearEquiv.ofFinrankEq (Module.finrank_fin_fun ℝ).symm
rw [← e.dimH_image]
refine le_antisymm ?_ ?_
· exact (dimH_mono (subset_univ _)).trans_eq (dimH_univ_pi_fin _)
· have : e '' s ∈ 𝓝 (e x) := by rw [← e.map_nhds_eq]; exact image_mem_map h
rcases Metric.nhds_basis_ball.mem_iff.1 this with ⟨r, hr0, hr⟩
simpa only [dimH_ball_pi_fin (e x) hr0] using dimH_mono hr
