Theorems · Theorem · measure theory

MeasureTheory.prob_compl_eq_one_sub

∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasurableSet s → μ sᶜ = 1 - μ s

Note that this is not quite as useful as it looks because the measure takes values in ℝ≥0∞. Thus the subtraction appearing is the truncated subtraction of ℝ≥0∞, rather than the better-behaved subtraction of ℝ.

Defined in

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

Cited by

4 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure