integrable

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.FinMeasSupp.integrable

English

If f.FinMeasSupp μ then f is integrable.

Русский

Если у функции FinMeasSupp, то она интегрируема.

LaTeX

$$$f\\mathrm{.FinMeasSupp}(\\mu) \\Rightarrow \\mathrm{Integrable}(f,\\mu)$$$

Lean4

theorem integrable {f : α →ₛ E} (h : f.FinMeasSupp μ) : Integrable f μ :=
  integrable_iff_finMeasSupp.2 h

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

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

Разделы

Аффилиация

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