pure_bind

Mathlib.Probability.ProbabilityMassFunction.Monad

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

← MathLib Explorer

English

For a fixed a, pure a.bind f = f a.

Русский

Для фиксированного a, (pure a).bind f = f(a).

LaTeX

$$$ (\mathrm{pure}\, a).\mathrm{bind} f = f(a) $$$

Lean4

@[simp]
theorem pure_bind (a : α) (f : α → PMF β) : (pure a).bind f = f a := by
  classical
  have : ∀ b a', ite (a' = a) (f a' b) 0 = ite (a' = a) (f a b) 0 := fun b a' => by split_ifs with h <;> simp [h]
  ext b
  simp [this]

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

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

Разделы

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

Аффилиация

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