le_hausdorffMeasure

Mathlib.MeasureTheory.Measure.Hausdorff

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.le_hausdorffMeasure

← MathLib Explorer

English

For d ∈ ℝ, μ ≤ μH[d] if for all s with diam s ≤ ε we have μ s ≤ (diam s)^d.

Русский

Для d ∈ ℝ, если для всех s с diam s ≤ ε выполняется μ s ≤ (diam s)^d, то μ ≤ μH[d].

LaTeX

$$$ μ ≤ μH[d] $$$

Lean4

theorem le_hausdorffMeasure (d : ℝ) (μ : Measure X) (ε : ℝ≥0∞) (h₀ : 0 < ε)
    (h : ∀ s : Set X, diam s ≤ ε → μ s ≤ diam s ^ d) : μ ≤ μH[d] :=
  le_mkMetric _ μ ε h₀ h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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