bind_pure

Mathlib.Probability.ProbabilityMassFunction.Monad

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

← MathLib Explorer

English

For any PMF p, p.bind pure = p.

Русский

Для любого PMF p, p.bind чистый = p.

LaTeX

$$$ p.\mathrm{bind} \mathrm{pure} = p $$$

Lean4

@[simp]
theorem bind_pure : p.bind pure = p :=
  PMF.ext fun x =>
    (bind_apply _ _ _).trans
      (_root_.trans (tsum_eq_single x fun y hy => by rw [pure_apply_of_ne _ _ hy.symm, mul_zero]) <| by
        rw [pure_apply_self, mul_one])

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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