dimH_le

Mathlib.Topology.MetricSpace.HausdorffDimension

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

English

If μH[d] s ≠ ∞, then dimH(s) ≤ d.

Русский

Если μ_H^d(s) не бесконечна, то dim_H(s) ≤ d.

LaTeX

$$dimH(s) \le d \quad \text{whenever} \quad μ_H[d](s) \neq ∞$$

Lean4

theorem dimH_le {s : Set X} {d : ℝ≥0∞} (H : ∀ d' : ℝ≥0, μH[d'] s = ∞ → ↑d' ≤ d) : dimH s ≤ d :=
  (dimH_def s).trans_le <| iSup₂_le H

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

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

Разделы

Аффилиация

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