toMeasure_inj — Mathlib

English

For PMFs p and q on α with a measurable singleton class, p.toMeasure = q.toMeasure if and only if p = q.

Русский

Для PMF p и q на α с измеримой одиничной частотой, p.toMeasure = q.toMeasure тогда и только тогда, когда p = q.

LaTeX

$$$\\forall p,q:\\ PMF(\\alpha),\\; p.toMeasure = q.toMeasure \\iff p = q.$$$

Lean4

@[simp]
theorem toMeasure_inj {p q : PMF α} : p.toMeasure = q.toMeasure ↔ p = q :=
  toMeasure_injective.eq_iff

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