setLIntegral_congr_fun — Mathlib

English

If f and g agree on s via EqOn, then the integrals over s are equal: ∫_s f = ∫_s g.

Русский

Если функции совпадают на s (EqOn), то интегралы по s совпадают: ∫_s f = ∫_s g.

LaTeX

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

Lean4

theorem setLIntegral_congr_fun {f g : α → ℝ≥0∞} {s : Set α} (hs : MeasurableSet s) (hfg : EqOn f g s) :
    ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ :=
  setLIntegral_congr_fun_ae hs <| Eventually.of_forall hfg

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