congr_set_ae — Mathlib

English

If f is integrable on t with respect to μ and s is μ-almost everywhere equal to t, then f is integrable on s with μ.

Русский

Если f интегрируема на t по μ и s равно t почти всюду по μ, то f интегрируема на s по μ.

LaTeX

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

Lean4

theorem congr_set_ae (h : IntegrableOn f t μ) (hst : s =ᵐ[μ] t) : IntegrableOn f s μ :=
  h.mono_set_ae hst.le

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