congr_fun — Mathlib

English

If f and g coincide on s (EqOn f g s) and s is measurable, then IntegrableOn f s μ if and only if IntegrableOn g s μ.

Русский

Если функции f и g совпадают на s (EqOn f g s) и множество s измеримо, то IntegrableOn f s μ эквивалентно IntegrableOn g s μ.

LaTeX

$$$\mathrm{EqOn}(f,g,s) \to \mathrm{MeasurableSet}(s) \to \mathrm{IntegrableOn}(f,s,\mu) \iff \mathrm{IntegrableOn}(g,s,\mu)$$$

Lean4

theorem congr_fun (h : IntegrableOn f s μ) (hst : EqOn f g s) (hs : MeasurableSet s) : IntegrableOn g s μ :=
  h.congr_fun_ae ((ae_restrict_iff' hs).2 (Eventually.of_forall hst))

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