congr_fun_ae — Mathlib

English

If f is integrable on s μ and f =ᵐ[μ.restrict s] g, then g is integrable on s μ.

Русский

Если f интегрируема на s по μ и f равно g почти наверху относительно μ|s, то g интегрируема на s по μ.

LaTeX

$$$\mathrm{IntegrableOn}(f,s,\mu) \to f =^{\mu|_s}_{\text{ae}} g \to \mathrm{IntegrableOn}(g,s,\mu)$$$

Lean4

theorem congr_fun_ae (h : IntegrableOn f s μ) (hst : f =ᵐ[μ.restrict s] g) : IntegrableOn g s μ :=
  Integrable.congr h hst

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