setIntegral_congr_ae₀ — Mathlib

English

If s is null-measurable and f equals g almost everywhere on s, then the integrals over s of f and g are equal.

Русский

Пусть s является нулево-измеримым множеством; если 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_ae₀ (hs : NullMeasurableSet s μ) (h : ∀ᵐ x ∂μ, x ∈ s → f x = g x) :
    ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ :=
  integral_congr_ae ((ae_restrict_iff'₀ hs).2 h)

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