locallyIntegrableOn — Mathlib

English

If f is locally integrable on μ, then it is locally integrable on any subset s with respect to the same μ.

Русский

Если функция f локально интегрируема по μ, то она локально интегрируема и на любом подмножестве s по той же мере μ.

LaTeX

$$$\\operatorname{LocallyIntegrable} f \\mu \\rightarrow \\forall s,\\ \\operatorname{LocallyIntegrableOn} f\\ s\\ \\mu$$$

Lean4

theorem locallyIntegrableOn (hf : LocallyIntegrable f μ) (s : Set X) : LocallyIntegrableOn f s μ := fun x _ =>
  (hf x).filter_mono nhdsWithin_le_nhds

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