integrableOn

Mathlib.MeasureTheory.Integral.IntegrableOn

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

English

If f is integrable on μ, then f is integrable on any measurable set s with μ restricted to s.

Русский

Если f интегрируема по мере μ, то она интегрируема на любом измеримом множестве s под ограниченной мерой μ|_s.

LaTeX

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

Lean4

theorem integrableOn (h : Integrable f μ) : IntegrableOn f s μ :=
  h.restrict

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

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

Разделы

Аффилиация

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