dimH_ball_pi_fin

Mathlib.Topology.MetricSpace.HausdorffDimension

URI: https://scilib.ai/kg/mathlib#Real.dimH_ball_pi_fin

English

Let x be a function Fin n → ℝ and r > 0. The Hausdorff dimension of the ball around x of radius r is n.

Русский

Пусть x ∈ Fin n → ℝ и r > 0. Размерность Хаусдорфа шара вокруг x радиуса r равна n.

LaTeX

$$$\\dim_H(\\mathrm{Ball}(x,r)) = n$$$

Lean4

theorem dimH_ball_pi_fin {n : ℕ} (x : Fin n → ℝ) {r : ℝ} (hr : 0 < r) : dimH (Metric.ball x r) = n := by
  rw [dimH_ball_pi x hr, Fintype.card_fin]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru