toMeasure_injective — Mathlib

English

Let α be a measurable space with a measurable singleton class. The mapping p ↦ p.toMeasure is injective; i.e., if p.toMeasure = q.toMeasure then p = q.

Русский

Пусть пространство α имеет измеримую одиничность; отображение p ↦ p.toMeasure инъективно: если p.toMeasure = q.toMeasure, то p = q.

LaTeX

$$$\\text{If } [\\text{MeasurableSingletonClass }\\alpha],\\; p,q:\\ PMF(\\alpha),\\; p.toMeasure = q.toMeasure \\Rightarrow p = q.$$$

Lean4

theorem toMeasure_injective : (toMeasure : PMF α → Measure α).Injective :=
  by
  intro p q h
  ext x
  rw [← p.toMeasure_apply_singleton x <| measurableSet_singleton x, ←
    q.toMeasure_apply_singleton x <| measurableSet_singleton x, h]

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