integrable_coeFn

Mathlib.MeasureTheory.Function.L1Space.AEEqFun

URI: https://scilib.ai/kg/mathlib#MeasureTheory.L1.integrable_coeFn

English

If f is in L1(μ), then f has finite integral with respect to μ.

Русский

Если f принадлежит L1(μ), то интеграл по μ конечен.

LaTeX

$$HasFiniteIntegral(f, μ)$$

Lean4

theorem integrable_coeFn (f : α →₁[μ] β) : Integrable f μ :=
  by
  rw [← memLp_one_iff_integrable]
  exact Lp.memLp f

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

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

Разделы

Аффилиация

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