integrableOn_congr_set_ae — Mathlib

English

If f is integrable on t μ and s equals t almost everywhere (μ), then f is integrable on s μ.

Русский

Если 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 integrableOn_congr_set_ae (hst : s =ᵐ[μ] t) : IntegrableOn f s μ ↔ IntegrableOn f t μ :=
  ⟨fun h ↦ h.congr_set_ae hst.symm, fun h ↦ h.congr_set_ae hst⟩

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