Theorems · Theorem · probability

ProbabilityTheory.HasLaw.ae_eq_of_dirac

∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {P : MeasureTheory.Measure Ω} [MeasurableSingletonClass 𝓧] {x : 𝓧},
  ProbabilityTheory.HasLaw X (MeasureTheory.Measure.dirac x) P → X =ᵐ[P] fun x_1 => x

Defined in

Mathlib.Probability.HasLaw

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasurableSingletonClass