mem_support_pure_iff

Mathlib.Probability.ProbabilityMassFunction.Monad

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

English

a' ∈ (pure a).support iff a' = a.

Русский

a' принадлежит поддержке чистого распределения тогда и только тогда, когда a' = a.

LaTeX

$$$ a' \in (\mathrm{pure}\, a).\mathrm{support} \iff a' = a $$$

Lean4

theorem mem_support_pure_iff : a' ∈ (pure a).support ↔ a' = a := by simp

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

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

Разделы

Аффилиация

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