ext

Mathlib.Probability.ProbabilityMassFunction.Basic

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

English

Two PMFs are equal if they agree on every outcome.

Русский

Два PMF равны тогда и только тогда, когда их значения совпадают для каждого исхода.

LaTeX

$$$\forall x, p x = q x \Rightarrow p = q$$$

Lean4

@[ext]
protected theorem ext {p q : PMF α} (h : ∀ x, p x = q x) : p = q :=
  DFunLike.ext p q h

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

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

Разделы

Аффилиация

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