coe_ne_zero

Mathlib.Probability.ProbabilityMassFunction.Basic

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

← MathLib Explorer

English

The coefficient function of a PMF is never identically zero.

Русский

Коэффициентная функция PMF не равна нулю как функция.

LaTeX

$$PMF.instFunLike.coe p ≠ 0$$

Lean4

@[simp]
theorem coe_ne_zero (p : PMF α) : ⇑p ≠ 0 := fun hp =>
  zero_ne_one ((tsum_zero.symm.trans (tsum_congr fun x => symm (congr_fun hp x))).trans p.tsum_coe)

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

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

Разделы

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

Аффилиация

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