integrable_iff_finMeasSupp

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

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

English

Integrable f μ is equivalent to f.FinMeasSupp μ for ENNReal p.

Русский

Интегрируемость эквивалентна FinMeasSupp для ENNReal p

LaTeX

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

Lean4

theorem integrable_iff_finMeasSupp {f : α →ₛ E} : Integrable f μ ↔ f.FinMeasSupp μ :=
  integrable_iff.trans finMeasSupp_iff.symm

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

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

Разделы

Аффилиация

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