eq_of_forall_toMeasure_apply_eq — Mathlib

English

If μ and ν agree on every measurable s, then μ = ν.

Русский

Если μ и ν согласны на каждом измеримом множестве, то μ = ν.

LaTeX

$$∀ μ ν, (∀ s, MeasurableSet(s) → (μ : Measure Ω) s = (ν : Measure Ω) s) → μ = ν$$

Lean4

@[ext]
theorem eq_of_forall_toMeasure_apply_eq (μ ν : ProbabilityMeasure Ω)
    (h : ∀ s : Set Ω, MeasurableSet s → (μ : Measure Ω) s = (ν : Measure Ω) s) : μ = ν :=
  by
  apply toMeasure_injective
  ext1 s s_mble
  exact h s s_mble

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