cond_cond_eq_cond_inter — Mathlib

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)

Похожие утверждения