bind_zero_right

Mathlib.MeasureTheory.Measure.GiryMonad

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

English

For any measure m on α, binding m with the zero-valued kernel yields the zero measure.

Русский

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

LaTeX

$$$\operatorname{bind}(m, 0) = 0$$$

Lean4

@[simp]
theorem bind_zero_right (m : Measure α) : bind m (0 : α → Measure β) = 0 :=
  bind_zero_right' m

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

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

Разделы

Аффилиация

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