setIntegral_congr_set — Mathlib

English

If s and t differ by a measure-zero set, the integrals of f over s and t are equal.

Русский

Если s и t отличаются нулевой мерой, интегралы по s и t равны.

LaTeX

$$$\\int_{x \\in s} f(x) \\,d\\mu = \\int_{x \\in t} f(x) \\,d\\mu \\quad\\text{whenever } μ(s\\triangle t)=0$$$

Lean4

theorem setIntegral_congr_set (hst : s =ᵐ[μ] t) : ∫ x in s, f x ∂μ = ∫ x in t, f x ∂μ := by
  rw [Measure.restrict_congr_set hst]

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