ext_of_lintegral — Mathlib

English

If for all measurable f the lintegrals with respect to μ and ν are equal, then μ = ν.

Русский

Если для всех измеримых f линегралы по μ и ν равны, то μ = ν.

LaTeX

$$$$ (\\forall f: α \\to \\mathbb{R}_{\\ge 0}^{\\infty}, Measurable f \\Rightarrow \\int^- a, f(a) \\ dμ = \\int^- a, f(a) \\ dν) \\Rightarrow μ = ν. $$$$

Lean4

theorem ext_of_lintegral (ν : Measure α) (hμν : ∀ f : α → ℝ≥0∞, Measurable f → ∫⁻ a, f a ∂μ = ∫⁻ a, f a ∂ν) : μ = ν :=
  (μ.ext_iff_lintegral ν).mpr hμν

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