memLp_iff_finMeasSupp

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.memLp_iff_finMeasSupp

← MathLib Explorer

English

MemLp is equivalent to FinMeasSupp for ENNReal p.

Русский

MemLp эквивалентно FinMeasSupp для p по ENNReal

LaTeX

$$$\\mathrm{MemLp}(f,p,\\mu) \\iff f\\mathrm{.FinMeasSupp}(\\mu)$$$

Lean4

theorem memLp_iff_finMeasSupp {f : α →ₛ E} (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) : MemLp f p μ ↔ f.FinMeasSupp μ :=
  (memLp_iff hp_pos hp_ne_top).trans finMeasSupp_iff.symm

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

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

Разделы

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

Аффилиация

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