measurable_coeFn

Mathlib.MeasureTheory.Function.L1Space.AEEqFun

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

English

Measurability transfers from L1 representative to the aeeq function cast.

Русский

Измеримость распространяется от представителя L1 к функций-эквиваленту.

LaTeX

$$Measurable_cast_from_L1$$

Lean4

@[fun_prop]
theorem measurable_coeFn [MeasurableSpace β] [BorelSpace β] (f : α →₁[μ] β) : Measurable f :=
  (Lp.stronglyMeasurable f).measurable

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

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

Разделы

Аффилиация

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