apply_eq_zero_iff — Mathlib

English

Let p be a probability mass function on α. Then for every a ∈ α, p(a) = 0 iff a ∉ supp(p).

Русский

Пусть p — функция массы вероятностей на α. Тогда для каждого a ∈ α выполняется p(a) = 0 тогда и только тогда, когда a ∉ опора(p).

LaTeX

$$$ \forall a : \alpha,\ p(a) = 0 \iff a \notin \mathrm{supp}(p). $$$

Lean4

theorem apply_eq_zero_iff (p : PMF α) (a : α) : p a = 0 ↔ a ∉ p.support := by rw [mem_support_iff, Classical.not_not]

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