Theorems · Theorem · probability

ProbabilityTheory.hasLaw_smul_dirac_of_ae_eq

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

Defined in

Mathlib.Probability.HasLaw

Cited by

2 results in Mathlib

Foundations

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