bind_zero_right'

Mathlib.MeasureTheory.Measure.GiryMonad

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

English

For any measure μ on α, binding μ with the constant zero-valued kernel gives the zero measure on β.

Русский

Для любой меры μ на α связывание μ с константной нулевой мерой на β даёт нулевую меру на β.

LaTeX

$$$\operatorname{bind}(\mu, x \mapsto 0) = 0$$$

Lean4

theorem bind_zero_right' (m : Measure α) : bind m (fun _ => 0 : α → Measure β) = 0 := by simp

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

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

Разделы

Аффилиация

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