toOuterMeasure_injective — Mathlib

English

The map sending a PMF to its outer measure is injective: if p.toOuterMeasure = q.toOuterMeasure then p = q.

Русский

Отображение PMF в его внешнюю меру инъективно: если p.toOuterMeasure = q.toOuterMeasure, то p = q.

LaTeX

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

Lean4

theorem toOuterMeasure_injective : (toOuterMeasure : PMF α → OuterMeasure α).Injective := fun p q h =>
  PMF.ext fun x =>
    (p.toOuterMeasure_apply_singleton x).symm.trans
      ((congr_fun (congr_arg _ h) _).trans <| q.toOuterMeasure_apply_singleton x)

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