dimH_coe_finset

Mathlib.Topology.MetricSpace.HausdorffDimension

URI: https://scilib.ai/kg/mathlib#dimH_coe_finset

English

For a finite set s, the Hausdorff dimension of s is zero.

Русский

Для конечного множества s размерность Хаусдорфа равна нулю.

LaTeX

$$$$\\dimH\\bigl((s : Set X)\\bigr) = 0.$$$$

Lean4

@[simp]
theorem dimH_coe_finset (s : Finset X) : dimH (s : Set X) = 0 :=
  s.finite_toSet.dimH_zero

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

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

Разделы

Аффилиация

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