English
If S is measurable and μ(S) ≠ ∞, then μ[|S][|T] = μ[|S ∩ T].
Русский
Если S измеримо и μ(S) ≠ ∞, то условное повторное условие равно условному на пересечение.
LaTeX
$$$\\text{MeasurableSet}(S) \\;\\land\\; μ(S) \\neq \\infty \\Rightarrow μ[|S][|T] = μ[|S \\cap T]$$$
Lean4
theorem cond_cond_eq_cond_inter' (hms : MeasurableSet s) (hmt : MeasurableSet t) (hcs : μ s ≠ ∞) :
μ[|s][|t] = μ[|s ∩ t] := by
ext u
obtain hst | hst := eq_or_ne (μ (s ∩ t)) 0
· have : μ (s ∩ t ∩ u) = 0 := measure_mono_null Set.inter_subset_left hst
simp [cond_apply, *, ← Set.inter_assoc]
· have hs : μ s ≠ 0 := (measure_pos_of_superset Set.inter_subset_left hst).ne'
simp [*, hms.inter hmt, cond_apply, ← Set.inter_assoc, ENNReal.mul_inv, ← mul_assoc, mul_comm _ (μ s)⁻¹,
ENNReal.inv_mul_cancel]