toOuterMeasure_inj

Mathlib.Probability.ProbabilityMassFunction.Basic

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

English

Equivalently, two PMFs have the same outer measure iff they are identical.

Русский

Эквивалентно: две PMF имеют одинаковую внешнюю меру тогда и только тогда, когда они тождественны.

LaTeX

$$$ p.toOuterMeasure = q.toOuterMeasure \iff p = q $$$

Lean4

@[simp]
theorem toOuterMeasure_inj {p q : PMF α} : p.toOuterMeasure = q.toOuterMeasure ↔ p = q :=
  toOuterMeasure_injective.eq_iff

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

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

Разделы

Аффилиация

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