toMeasure_pure_apply — Mathlib

English

For countable α, measurable singleton, the dirac measure corresponds to the pure PMF.

Русский

Для счетного типа α и измеримой одиночки мера Дирака соответствует чистому PMF.

LaTeX

$$$ (\mathrm{Measure.dirac}\, a).\mathrm{toPMF} = \mathrm{PMF.pure}(a) $$$

Lean4

/-- The measure of a set under `pure a` is `1` for sets containing `a` and `0` otherwise. -/
@[simp]
theorem toMeasure_pure_apply (hs : MeasurableSet s) : (pure a).toMeasure s = if a ∈ s then 1 else 0 :=
  (toMeasure_apply_eq_toOuterMeasure_apply (pure a) hs).trans (toOuterMeasure_pure_apply a s)

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