restrict — Mathlib

English

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

Русский

Если f интегрируема на s по μ и f эквивалентна g по μ|s almost everywhere, то g интегрируема на s по μ.

LaTeX

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

Lean4

theorem restrict (h : IntegrableOn f s μ) : IntegrableOn f s (μ.restrict t) :=
  by
  dsimp only [IntegrableOn] at h ⊢
  exact h.mono_measure <| Measure.restrict_mono_measure Measure.restrict_le_self _

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