hasFiniteIntegral_coeFn

Mathlib.MeasureTheory.Function.L1Space.AEEqFun

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

English

For f in L1, the associated function is strongly measurable.

Русский

Для функции в L1 соответствующая функция сильна измерима.

LaTeX

$$StronglyMeasurable(f) in L1$$

Lean4

theorem hasFiniteIntegral_coeFn (f : α →₁[μ] β) : HasFiniteIntegral f μ :=
  (integrable_coeFn f).hasFiniteIntegral

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

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

Разделы

Аффилиация

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