integrable_of_isFiniteMeasure

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

← MathLib Explorer

English

If μ is finite, then every simple function is integrable.

Русский

Если мера конечна, то любая простая функция интегрируема.

LaTeX

$$$[IsFiniteMeasure\\,\\mu] \\Rightarrow \\mathrm{Integrable}(f,\\mu)$$$

Lean4

@[fun_prop]
theorem integrable_of_isFiniteMeasure [IsFiniteMeasure μ] (f : α →ₛ E) : Integrable f μ :=
  memLp_one_iff_integrable.mp (f.memLp_of_isFiniteMeasure 1 μ)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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