Theorems · Theorem · probability

MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le

∀ (Ω : Type u_1) [inst : PseudoMetricSpace Ω] [inst_1 : MeasurableSpace Ω] [OpensMeasurableSpace Ω]
  [TopologicalSpace.SeparableSpace Ω] {ε : ℝ},
  0 < ε →
    ∃ As,
      (∀ (n : ℕ), MeasurableSet (As n)) ∧
        (∀ (n : ℕ), Bornology.IsBounded (As n)) ∧
          (∀ (n : ℕ), Metric.diam (As n) ≤ ε) ∧ ⋃ n, As n = Set.univ ∧ Pairwise fun n m => Disjoint (As n) (As m)

In a separable pseudometric space, for any ε > 0 there exists a countable collection of disjoint Borel measurable subsets of diameter at most ε that cover the whole space.

Defined in

Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Cited by

1 results in Mathlib

Foundations

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

Assumes

PseudoMetricSpaceMeasurableSpaceOpensMeasurableSpaceTopologicalSpace.SeparableSpace