bind_dirac — Mathlib

English

For any measure m on α, binding with the Dirac measure produces the original measure, i.e., bind m dirac = m.

Русский

Для любой меры m на α связывание с Дираковой мерой восстанавливает исходную меру: bind m dirac = m.

LaTeX

$$$\\mathrm{bind}\\, m\\, \\mathrm{dirac} = m$$$

Lean4

@[simp]
theorem bind_dirac {m : Measure α} : bind m dirac = m :=
  by
  ext1 s hs
  simp only [bind_apply hs measurable_dirac.aemeasurable, dirac_apply' _ hs, lintegral_indicator hs, Pi.one_apply,
    lintegral_one, restrict_apply, MeasurableSet.univ, univ_inter]

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