bindOnSupport_pure

Mathlib.Probability.ProbabilityMassFunction.Monad

URI: https://scilib.ai/kg/mathlib#PMF.bindOnSupport_pure

English

Binding p with the map a ↦ pure a returns p: (p.bindOnSupport (λ a, pure a)) = p.

Русский

Связывание p по отображению a ↦ pure a возвращает p: (p.bindOnSupport (λ a, pure a)) = p.

LaTeX

$$$$ (\\mathrm{bindOnSupport}(p, \\lambda a. \\mathrm{pure}(a))) = p $$$$

Lean4

theorem bindOnSupport_pure (p : PMF α) : (p.bindOnSupport fun a _ => pure a) = p := by
  simp only [PMF.bind_pure, PMF.bindOnSupport_eq_bind]

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

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

Разделы

Аффилиация

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