aestronglyMeasurable_coeFn

Mathlib.MeasureTheory.Function.L1Space.AEEqFun

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

English

If f is AEStronglyMeasurable, Integrable.mk f hf is equivalent to integrability of f.

Русский

Если f имеет AEStronglyMeasurable, то Integrable.mk f hf эквивалентна интегрируемости f.

LaTeX

$$Integrable.mk f hf integrable_iff$$

Lean4

@[fun_prop]
theorem aestronglyMeasurable_coeFn (f : α →₁[μ] β) : AEStronglyMeasurable f μ :=
  Lp.aestronglyMeasurable f

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

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

Разделы

Аффилиация

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