join_dirac

Mathlib.MeasureTheory.Measure.GiryMonad

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.join_dirac

English

Join of a Dirac measure recovers the original measure: join (dirac μ) = μ.

Русский

Связка (join) для мер Дирака возвращает исходную меру: join (dirac μ) = μ.

LaTeX

$$$\\mathrm{join}(\\mathrm{dirac}\\,\\mu) = \\mu.$$$

Lean4

@[simp]
theorem join_dirac (μ : Measure α) : join (dirac μ) = μ :=
  by
  ext s hs
  simp [hs, lintegral_dirac', measurable_coe]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru