Theorems · Theorem · probability

MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt

∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] {μ ν : MeasureTheory.Measure Ω}
  {c : ENNReal},
  MeasureTheory.levyProkhorovEDist μ ν < c → ∀ {B : Set Ω}, MeasurableSet B → μ B ≤ ν (Metric.thickening c.toReal B) + c

Defined in

Mathlib.MeasureTheory.Measure.LevyProkhorovMetric

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSpacePseudoEMetricSpace