integral_congr_ae_restrict — Mathlib

English

Similar to previous congruence, with a restricted almost-everywhere equality.

Русский

Аналогично предыдущему, для равенства почти всюду при ограниченной мере.

LaTeX

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

Lean4

/-- Integrals are equal for functions that agree almost everywhere for the restricted measure. -/
theorem integral_congr_ae_restrict {a b : ℝ} {f g : ℝ → E} {μ : Measure ℝ} (h : f =ᵐ[μ.restrict (Ι a b)] g) :
    ∫ x in a..b, f x ∂μ = ∫ x in a..b, g x ∂μ :=
  integral_congr_ae (ae_imp_of_ae_restrict h)

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