toPMF_dirac — Mathlib

English

Under mild hypotheses, the PMF corresponding to the dirac measure is pure at a.

Русский

При умеренных предположениях PMF, соответствующее мере Дирака, сосредоточено в точке a.

LaTeX

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

Lean4

@[simp]
theorem toPMF_dirac [Countable α] [h : MeasurableSingletonClass α] : (Measure.dirac a).toPMF = pure a := by
  rw [toPMF_eq_iff_toMeasure_eq, toMeasure_pure]

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