setLIntegral_congr_fun_ae — Mathlib

English

If hs is measurable and hfg expresses that f and g are equal almost everywhere on s, then the restricted integrals over s are equal: ∫_s f = ∫_s g.

Русский

Пусть s измеримо и f и g равны почти в каждой точке на s, тогда интегралы по s равны: ∫_s f = ∫_s g.

LaTeX

$$$\\int_s f \\! d\\mu = \\int_s g \\! d\\mu$$$

Lean4

theorem setLIntegral_congr_fun_ae {f g : α → ℝ≥0∞} {s : Set α} (hs : MeasurableSet s)
    (hfg : ∀ᵐ x ∂μ, x ∈ s → f x = g x) : ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ :=
  by
  rw [lintegral_congr_ae]
  rw [EventuallyEq]
  rwa [ae_restrict_iff' hs]

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