English
Two finite Borel measures μ and ν are equal if they integrate all bounded continuous real-valued functions f: Ω → ℝ in the same way.
Русский
Две конечные Борелевские меры μ и ν равны, если интегралы от всех ограниченных непрерывных функций в ℝ совпадают по обеим мерам.
LaTeX
$$μ = ν if ∀ f : Ω →ᵇ ℝ, ∫ f dμ = ∫ f dν.$$
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_of_IsFiniteMeasure {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω]
[HasOuterApproxClosed Ω] [BorelSpace Ω] {μ ν : Measure Ω} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
(h : ∀ (f : Ω →ᵇ ℝ), ∫ x, f x ∂μ = ∫ x, f x ∂ν) : μ = ν :=
by
apply ext_of_forall_lintegral_eq_of_IsFiniteMeasure
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'⟩
