cond_mul_eq_inter' — Mathlib

English

μ[T|S] ⋅ μ(S) = μ(S ∩ T) when S is measurable and μ(S) ≠ ∞.

Русский

μ[T|S] ⋅ μ(S) = μ(S ∩ T), если S измеримо и μ(S) ≠ ∞.

LaTeX

$$$\\text{MeasurableSet}(S) \\land μ(S) \\neq ∞ \\Rightarrow μ[T|S] \\cdot μ(S) = μ(S \\cap T)$$$

Lean4

theorem cond_mul_eq_inter' (hms : MeasurableSet s) (hcs' : μ s ≠ ∞) (t : Set Ω) : μ[t | s] * μ s = μ (s ∩ t) :=
  by
  obtain hcs | hcs := eq_or_ne (μ s) 0
  · simp [hcs, measure_inter_null_of_null_left]
  · rw [cond_apply hms, mul_comm, ← mul_assoc, ENNReal.mul_inv_cancel hcs hcs', one_mul]

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