ext_fun — Mathlib

English

If for all a and all nonnegative measurable f, ∫ f dκ a = ∫ f dη a, then κ = η.

Русский

Если для всех a и всех неотрицательных измеримых функций f выполняется ∫ f dκ a = ∫ f dη a, то κ = η.

LaTeX

$$$\\forall a \\forall f\\ (Measurable f \\rightarrow \\\\int f \\\\mathrm{d}\\\\kappa a = \\\\int f \\\\mathrm{d}\\\\eta a) \\\\Rightarrow \\\\kappa = \\\\eta$$$

Lean4

theorem ext_fun (h : ∀ a f, Measurable f → ∫⁻ b, f b ∂κ a = ∫⁻ b, f b ∂η a) : κ = η :=
  by
  ext a s hs
  specialize h a (s.indicator fun _ => 1) (Measurable.indicator measurable_const hs)
  simp_rw [lintegral_indicator_const hs, one_mul] at h
  rw [h]

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