cond_pos_of_inter_ne_zero — Mathlib

English

If S is measurable and μ(S) < ∞, then μ([·|S][·|T]) = μ(·|S ∩ T).

Русский

Если S измеримо и μ(S) < ∞, то μ после двух условных преобразований равна μ по пересечению S и T.

LaTeX

$$$\\text{MeasurableSet}(S) \\rightarrow μ[|S][|T] = μ[|S \\cap T] \\quad\\text{(provided } μ(S) \\neq \\infty\\text{)}$$$

Lean4

theorem cond_pos_of_inter_ne_zero [IsFiniteMeasure μ] (hms : MeasurableSet s) (hci : μ (s ∩ t) ≠ 0) : 0 < μ[t | s] :=
  by
  rw [cond_apply hms]
  refine ENNReal.mul_pos ?_ hci
  exact ENNReal.inv_ne_zero.mpr (measure_ne_top _ _)

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