support_bind

Mathlib.Probability.ProbabilityMassFunction.Monad

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

← MathLib Explorer

English

The support of p.bind f equals the union over a ∈ p.support of (f a).support.

Русский

support(p.bind f) = ⋃_{a ∈ support(p)} support(f(a)).

LaTeX

$$$ (p.\mathrm{bind} f).\mathrm{support} = \bigcup_{a \in p.\mathrm{support}} (f(a)).\mathrm{support} $$$

Lean4

@[simp]
theorem support_bind : (p.bind f).support = ⋃ a ∈ p.support, (f a).support :=
  Set.ext fun b => by simp [mem_support_iff, ENNReal.tsum_eq_zero, not_or]

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

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

Разделы

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

Аффилиация

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