support_pure

Mathlib.Probability.ProbabilityMassFunction.Monad

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

English

For any a, the support of pure a is the singleton {a}.

Русский

Для любого a поддержка чистого распределения p = pure a равна одиночному множеству {a}.

LaTeX

$$$ (\mathrm{pure\} a).\mathrm{support} = \{ a \} $$$

Lean4

@[simp]
theorem support_pure : (pure a).support = { a } :=
  Set.ext fun a' => by simp [mem_support_iff]

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

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

Разделы

Аффилиация

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