toMeasure_injective — Mathlib

English

The map sending a probability measure to its underlying measure is injective: if μ.toMeasure = ν.toMeasure, then μ = ν.

Русский

Отображение распределения к соответствующей мере инъективно: если их базовые меры совпадают, то сами распределения совпадают.

LaTeX

$$∀ μ ν, μ.toMeasure = ν.toMeasure → μ = ν$$

Lean4

theorem toMeasure_injective : Function.Injective ((↑) : ProbabilityMeasure Ω → Measure Ω) :=
  Subtype.coe_injective

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