locallyIntegrable

Mathlib.MeasureTheory.Function.LocallyIntegrable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Integrable.locallyIntegrable

English

If f is integrable with respect to μ, then f is locally integrable with respect to μ.

Русский

Если функция f интегрируема по μ, то она локально интегрируема по μ.

LaTeX

$$$\\operatorname{Integrable} f\\mu \\Rightarrow \\operatorname{LocallyIntegrable} f\\mu$$$

Lean4

theorem locallyIntegrable (hf : Integrable f μ) : LocallyIntegrable f μ := fun _ => hf.integrableAtFilter _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru