cond_mul_eq_inter — Mathlib

English

General form: μ[T|S] ⋅ μ(S) = μ(S ∩ T) for measurable S and IsFinite μ.

Русский

Общая форма: μ[T|S] ⋅ μ(S) = μ(S ∩ T) для измеримого S и конечной меры μ.

LaTeX

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

Lean4

theorem cond_mul_eq_inter (hms : MeasurableSet s) (t : Set Ω) (μ : Measure Ω) [IsFiniteMeasure μ] :
    μ[t | s] * μ s = μ (s ∩ t) :=
  cond_mul_eq_inter' hms (measure_ne_top _ s) t

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