English
Two finite measures μ, ν on Ω are equal if the integrals of all bounded continuous functions against μ and ν coincide.
Русский
Два конечных меры μ и ν на Ω равны тогда и только тогда, когда интегралы по всем ограниченным непрерывным функциям совпадают.
LaTeX
$$$\forall f : Ω \to ℝ,\ \int f \, dμ = \int f \, dν \Rightarrow μ = ν$$$
Lean4
/-- Two finite Borel measures are equal if the integrals of all bounded continuous functions with
respect to both agree. -/
theorem ext_of_forall_integral_eq [HasOuterApproxClosed Ω] [BorelSpace Ω] {μ ν : FiniteMeasure Ω}
(h : ∀ (f : Ω →ᵇ ℝ), ∫ x, f x ∂μ = ∫ x, f x ∂ν) : μ = ν :=
by
apply ext_of_forall_lintegral_eq
intro f
apply (ENNReal.toReal_eq_toReal_iff' (lintegral_lt_top_of_nnreal μ f).ne (lintegral_lt_top_of_nnreal ν f).ne).mp
rw [toReal_lintegral_coe_eq_integral f μ, toReal_lintegral_coe_eq_integral f ν]
exact h ⟨⟨fun x => (f x).toReal, Continuous.comp' NNReal.continuous_coe f.continuous⟩, f.map_bounded'⟩
