setIntegral_congr_fun — Mathlib

English

If f equals g on a measurable set s, then the integrals over s of f and g are equal.

Русский

Если f равно g на измеримом множестве s, то интегралы по s совпадают.

LaTeX

$$$\\int_{x \\in s} f(x) \\,d\\mu = \\int_{x \\in s} g(x) \\,d\\mu$$$

Lean4

theorem setIntegral_congr_fun (hs : MeasurableSet s) (h : EqOn f g s) : ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ :=
  setIntegral_congr_ae hs <| Eventually.of_forall h

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