cond_inter_self — Mathlib

English

If S is measurable and T is any subset, then conditioning on S preserves intersections: μ[S ∩ T | S] = μ[T | S].

Русский

Если S измеримо, а T любая подмножество, то условная вероятность пересечения с S равна условной вероятности T при условии S.

LaTeX

$$$\\text{MeasurableSet}(S) \\;\Rightarrow\\; \\mu[S \\cap T \\mid S] = \\mu[T \\mid S]$$$

Lean4

theorem cond_inter_self (hms : MeasurableSet s) (t : Set Ω) (μ : Measure Ω) : μ[s ∩ t | s] = μ[t | s] := by
  rw [cond_apply hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply hms]

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