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]