hausdorffMeasure_apply — Mathlib

English

μH[d] s is given by mkMetric_apply with supremums over r and refinements t.

Русский

μH[d] s задаётся через mkMetric_apply с верхними пределами по r и разложениям t.

LaTeX

$$$ μH[d] s = mkMetric_apply\, m (d) (s) $$$

Lean4

/-- A formula for `μH[d] s`. -/
theorem hausdorffMeasure_apply (d : ℝ) (s : Set X) :
    μH[d] s =
      ⨆ (r : ℝ≥0∞) (_ : 0 < r),
        ⨅ (t : ℕ → Set X) (_ : s ⊆ ⋃ n, t n) (_ : ∀ n, diam (t n) ≤ r), ∑' n, ⨆ _ : (t n).Nonempty, diam (t n) ^ d :=
  mkMetric_apply _ _

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