English
Conditioning successively on S and then on T equals conditioning on S ∩ T when S,T are measurable and μ(S) < ∞.
Русский
Условление последовательно на S и затем на T равняется условному на S ∩ T при измеримости S и T и μ(S) < ∞.
LaTeX
$$$\\text{MeasurableSet}(S) \\land \\text{MeasurableSet}(T) \\land μ(S) \\neq ∞ \\Rightarrow μ[|S][|T] = μ[|S \\cap T]$$$
Lean4
/-- Conditioning first on `s` and then on `t` results in the same measure as conditioning
on `s ∩ t`. -/
theorem cond_cond_eq_cond_inter (hms : MeasurableSet s) (hmt : MeasurableSet t) (μ : Measure Ω) [IsFiniteMeasure μ] :
μ[|s][|t] = μ[|s ∩ t] :=
cond_cond_eq_cond_inter' hms hmt (measure_ne_top μ s)