integral_congr_ae — Mathlib

English

If two functions f and g are almost everywhere equal, their integrals are equal.

Русский

Если две функции равны почти везде, их интегралы равны.

LaTeX

$$$(\text{ae }\mu).\text{EventuallyEq} f g \Rightarrow \int a, f a \partial\mu = \int a, g a \partial\mu$$$

Lean4

theorem integral_congr_ae {f g : α → G} (h : f =ᵐ[μ] g) : ∫ a, f a ∂μ = ∫ a, g a ∂μ :=
  by
  by_cases hG : CompleteSpace G
  · simp only [integral, hG, L1.integral]
    exact setToFun_congr_ae (dominatedFinMeasAdditive_weightedSMul μ) h
  · simp [integral, hG]

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