Documentation
PFR
.
Mathlib
.
Probability
.
ConditionalProbability
Search
Google site search
return to top
source
Imports
Init
Mathlib.Probability.ConditionalProbability
Imported by
PFR
PFR.RhoFunctional
ProbabilityTheory
.
ae_cond_mem
source
theorem
ProbabilityTheory
.
ae_cond_mem
{Ω :
Type
u_1}
{mΩ :
MeasurableSpace
Ω
}
{μ :
MeasureTheory.Measure
Ω
}
{s :
Set
Ω
}
(hs :
MeasurableSet
s
)
:
∀ᵐ (
x
:
Ω
) ∂
ProbabilityTheory.cond
μ
s
,
x
∈
s