Theorems · Theorem · measure theory

MeasureTheory.Measure.mkMetric_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)] (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) →
          ∀ (m : ENNReal → ENNReal),
            (MeasureTheory.Measure.mkMetric m) s ≤ Filter.liminf (fun n => ∑' (i : ι n), m (Metric.ediam (t n i))) l

To bound the Hausdorff measure (or, more generally, for a measure defined using MeasureTheory.Measure.mkMetric) 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

2 results in Mathlib

Foundations

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

Assumes

EMetricSpaceMeasurableSpaceBorelSpaceCountable