eq_of_cdf — Mathlib

English

If two probability measures μ and ν on ℝ have the same cdf, then μ = ν.

Русский

Если две вероятностные меры μ и ν на ℝ имеют одинаковую функцию распределения, то μ = ν.

LaTeX

$$$ \text{cdf}(\mu) = \text{cdf}(\nu) \;\Rightarrow\; \mu = \nu $$$

Lean4

/-- If two real probability distributions have the same cdf, they are equal. -/
theorem eq_of_cdf (μ ν : Measure ℝ) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (h : cdf μ = cdf ν) : μ = ν := by
  rw [← measure_cdf μ, ← measure_cdf ν, h]

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