apply_pos_iff

Mathlib.Probability.ProbabilityMassFunction.Basic

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

English

For any a ∈ α, p(a) > 0 iff a ∈ supp(p).

Русский

Для любого a ∈ α верно: p(a) > 0 тогда и только тогда, когда a ∈ опора(p).

LaTeX

$$$ 0 < p(a) \iff a \in \mathrm{supp}(p). $$$

Lean4

theorem apply_pos_iff (p : PMF α) (a : α) : 0 < p a ↔ a ∈ p.support :=
  pos_iff_ne_zero.trans (p.mem_support_iff a).symm

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

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

Разделы

Аффилиация

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