cond_apply — Mathlib

English

Replacing by the measurable hull does not change the conditional measure.

Русский

Заменить множество на измеримую оболочку не меняет условную меру.

LaTeX

$$$cond\\_toMeasurable\\_eq$$$

Lean4

/-- The axiomatic definition of conditional probability derived from a measure-theoretic one. -/
theorem cond_apply (hms : MeasurableSet s) (μ : Measure Ω) (t : Set Ω) : μ[t | s] = (μ s)⁻¹ * μ (s ∩ t) := by
  rw [cond, Measure.smul_apply, Measure.restrict_apply' hms, Set.inter_comm, smul_eq_mul]

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