Theorems · Theorem · measure theory

MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum

∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {β : Type u_4}
  {ι : β → Type u_5} [∀ (n : β), Countable (ι n)] (d : ℝ) (s : Set X) {l : Filter β} (r : β → ENNReal),
  Filter.Tendsto r l (nhds 0) →
    ∀ (t : (n : β) → ι n → Set X),
      (∀ᶠ (n : β) in l, ∀ (i : ι n), Metric.ediam (t n i) ≤ r n) →
        (∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) →
          (MeasureTheory.Measure.hausdorffMeasure d) s ≤
            Filter.liminf (fun n => ∑' (i : ι n), Metric.ediam (t n i) ^ d) l

To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending to 0, indexed by any sequence of countable types.

Defined in

Mathlib.MeasureTheory.Measure.Hausdorff

Cited by

0 results in Mathlib

Foundations

Depth 201 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

EMetricSpaceMeasurableSpaceBorelSpaceCountable