integral_congr_ae' — Mathlib

English

If f and g are almost everywhere equal with respect to μ restricted to I, then their interval integrals over I coincide.

Русский

Если f и g равны почти всюду по отношению к мере, ограниченной на интервал I, их интервальные интегралы равны.

LaTeX

$$$ (f =^{\\text{ae}}_{\\mu\\restriction I} g) \\Rightarrow \\int_{I} f \\, dμ = \\int_{I} g \\, dμ $$$

Lean4

theorem integral_congr_ae' (h : ∀ᵐ x ∂μ, x ∈ Ioc a b → f x = g x) (h' : ∀ᵐ x ∂μ, x ∈ Ioc b a → f x = g x) :
    ∫ x in a..b, f x ∂μ = ∫ x in a..b, g x ∂μ := by
  simp only [intervalIntegral, setIntegral_congr_ae measurableSet_Ioc h, setIntegral_congr_ae measurableSet_Ioc h']

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