eq_of_le_of_isProbabilityMeasure — Mathlib

English

If μ ≤ ν and both are probability measures, then μ = ν.

Русский

Если μ ≤ ν и обе меры вероятностны, то μ = ν.

LaTeX

$$$\mu \leq \nu \;\Rightarrow\; \mu = \nu \quad\text{при } [\text{IsProbabilityMeasure }\mu] [\text{IsProbabilityMeasure }\nu]$$$

Lean4

theorem eq_of_le_of_isProbabilityMeasure {μ ν : Measure α} [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
    (hμν : μ ≤ ν) : μ = ν :=
  eq_of_le_of_measure_univ_eq hμν (by simp)

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