aestronglyMeasurable

Mathlib.MeasureTheory.Function.LpSeminorm.Defs

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MemLp.aestronglyMeasurable

English

If a function f belongs to Lp, then it is AEStronglyMeasurable with respect to μ.

Русский

Если функция f принадлежит Lp, то она AEStronglyMeasurable по отношению к μ.

LaTeX

$$$\\text{AEStronglyMeasurable}(f,\\mu)$$$

Lean4

theorem aestronglyMeasurable [TopologicalSpace ε] {f : α → ε} {p : ℝ≥0∞} (h : MemLp f p μ) : AEStronglyMeasurable f μ :=
  h.1

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

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

Разделы

Аффилиация

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