memLp

Mathlib.MeasureTheory.Function.SimpleFuncDenseLp

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Lp.simpleFunc.memLp

← MathLib Explorer

English

The a.e. equality between toSimpleFunc f and f holds: toSimpleFunc f =ᵐμ f.

Русский

С Hessen a.e. равенство: toSimpleFunc f =ᵐμ f.

LaTeX

$$$\mathrm{toSimpleFunc}(f) =_{\mu} f$$$

Lean4

/-- `toSimpleFunc f` satisfies the predicate `MemLp`. -/
protected theorem memLp (f : Lp.simpleFunc E p μ) : MemLp (toSimpleFunc f) p μ :=
  MemLp.ae_eq (toSimpleFunc_eq_toFun f).symm <| mem_Lp_iff_memLp.mp (f : Lp E p μ).2

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

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

Разделы

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

Аффилиация

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