integrableOn_congr_fun — Mathlib

English

If there exists an ae equality of f and g on s with respect to μ.restrict s, then IntegrableOn f s μ if and only if IntegrableOn g s μ.

Русский

Если существует ae-эквивалентность f и g на s относительно μ|s, то интеграбельность на s одинаково для f и g.

LaTeX

$$$ (\mathrm{ae}(\mu|_s))\ eventuallyEq f g \to \mathrm{IntegrableOn}(f,s,\mu) \iff \mathrm{IntegrableOn}(g,s,\mu)$$$

Lean4

theorem integrableOn_congr_fun (hst : EqOn f g s) (hs : MeasurableSet s) : IntegrableOn f s μ ↔ IntegrableOn g s μ :=
  ⟨fun h => h.congr_fun hst hs, fun h => h.congr_fun hst.symm hs⟩

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