join_eq_bind

Mathlib.MeasureTheory.Measure.GiryMonad

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

English

In the Giry monad, the join of a measure of measures is equal to binding by the identity: join μ = μ.bind id.

Русский

В Giry-монаде объединение меры множеств равно связыванию по тождественности: join μ = μ.bind id.

LaTeX

$$$\\mathrm{join}\\,\\mu = \\mathrm{bind}\\,\\mu\\, \\mathrm{id}$$$

Lean4

theorem join_eq_bind (μ : Measure (Measure α)) : join μ = bind μ id := by rw [bind, map_id]

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

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

Разделы

Аффилиация

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