eq_of_forall_toMeasure_apply_eq — Mathlib

English

If μ and ν are FiniteMeasure and μ.toMeasure(s) = ν.toMeasure(s) for all measurable s, then μ = ν.

Русский

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

LaTeX

$$theorem eq_of_forall_apply_eq (μ ν : FiniteMeasure Ω) (h : ∀ s, MeasurableSet s → μ s = ν s) : μ = ν$$

Lean4

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

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