mono_set_ae — Mathlib

English

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

Русский

Если f интегрируема на t по μ и s ∈μ-a.e. содержится в t, то f интегрируема на s по μ.

LaTeX

$$$\mathrm{IntegrableOn}(f,t,\mu) \to s \leq_{\mu} t \to \mathrm{IntegrableOn}(f,s,\mu)$$$

Lean4

theorem mono_set_ae (h : IntegrableOn f t μ) (hst : s ≤ᵐ[μ] t) : IntegrableOn f s μ :=
  h.integrable.mono_measure <| Measure.restrict_mono_ae hst

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