English
Two finite Borel measures μ and ν are equal if they integrate all nonnegative bounded continuous functions f: Ω → NNReal in the same way.
Русский
Две конечные Борелевские меры μ и ν равны, если для всех неотрицательных ограниченных непрерывных функций f: Ω → NNReal интегралы совпадают.
LaTeX
$$μ = ν if ∀ f : Ω →ᵇ NNReal, ∫ f dμ = ∫ f dν.$$
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_of_IsFiniteMeasure {Ω : Type*} [MeasurableSpace Ω] [TopologicalSpace Ω]
[HasOuterApproxClosed Ω] [BorelSpace Ω] {μ ν : Measure Ω} [IsFiniteMeasure μ]
(h : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ x, f x ∂μ = ∫⁻ x, f x ∂ν) : μ = ν :=
by
have key := @measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure Ω _ _ _ _ μ ν _ h
apply ext_of_generate_finite _ ?_ isPiSystem_isClosed
· exact fun F F_closed ↦ key F_closed
· exact key isClosed_univ
· rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]
