toMeasure_eq_iff_eq_toPMF — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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