stronglyMeasurable_coeFn

Mathlib.MeasureTheory.Function.L1Space.AEEqFun

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

English

For f in L1, the associated function is measurable.

Русский

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

LaTeX

$$Measurable(f) in L1$$

Lean4

@[fun_prop]
theorem stronglyMeasurable_coeFn (f : α →₁[μ] β) : StronglyMeasurable f :=
  Lp.stronglyMeasurable f

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

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

Разделы

Аффилиация

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