aemeasurable

Mathlib.MeasureTheory.Function.LpSeminorm.Defs

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

← MathLib Explorer

English

If f is MemLp(f,p,μ), then f is AEMeasurable with respect to μ.

Русский

Если f ∈ MemLp(f,p,μ), то f — AEMeasurable по отношению к μ.

LaTeX

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

Lean4

theorem aemeasurable [MeasurableSpace ε] [TopologicalSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε] [BorelSpace ε]
    {f : α → ε} {p : ℝ≥0∞} (hf : MemLp f p μ) : AEMeasurable f μ :=
  hf.aestronglyMeasurable.aemeasurable

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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