Documentation

PFR.Mathlib.Probability.ConditionalProbability

theorem ProbabilityTheory.ae_cond_mem {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω} (hs : MeasurableSet s) :
∀ᵐ (x : Ω) ∂ProbabilityTheory.cond μ s, x s