ext_of_forall_lintegral_eq — Mathlib

English

Two finite measures μ, ν on Ω are equal if the integrals of all nonnegative bounded continuous functions against μ and ν agree.

Русский

Два конечных мер μ и ν на Ω равны тогда и только тогда, когда интегралы по всем неотрицательным ограниченным непрерывным функциям совпадают.

LaTeX

$$$\forall f : Ω \to_b ℝ≥0,\ ∫⁻ x f(x) \mathrm{d}μ = ∫⁻ x f(x) \mathrm{d}ν \Rightarrow μ = ν$$$

Lean4

/-- Two finite Borel measures are equal if the integrals of all non-negative bounded continuous
functions with respect to both agree. -/
theorem ext_of_forall_lintegral_eq [HasOuterApproxClosed Ω] [BorelSpace Ω] {μ ν : FiniteMeasure Ω}
    (h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ x, f x ∂μ = ∫⁻ x, f x ∂ν) : μ = ν :=
  by
  apply Subtype.ext
  change (μ : Measure Ω) = (ν : Measure Ω)
  exact ext_of_forall_lintegral_eq_of_IsFiniteMeasure h

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