toPMF_eq_iff_toMeasure_eq

Mathlib.Probability.ProbabilityMassFunction.Basic

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

← MathLib Explorer

English

For PMF p and a probability measure μ, μ.toPMF = p if and only if μ = p.toMeasure.

Русский

Для вероятностной меры μ и PMF p верно: μ.toPMF = p тогда и только тогда, μ = p.toMeasure.

LaTeX

$$$ \\mu.toPMF = p \\iff \\mu = p.toMeasure $$$

Lean4

theorem toPMF_eq_iff_toMeasure_eq (μ : Measure α) [IsProbabilityMeasure μ] : μ.toPMF = p ↔ μ = p.toMeasure := by
  rw [← toMeasure_inj, Measure.toPMF_toMeasure]

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

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

Разделы

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

Аффилиация

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