toLp_coeFn

Mathlib.MeasureTheory.Function.LpSpace.Basic

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

English

Equality of eLpNorm for a function and its AEEqFun representation for any AEStronglyMeasurable f.

Русский

Равенство eLpNorm между функцией и её представлением через AEEqFun для любой AEStronglyMeasurable f.

LaTeX

$$eLpNorm (AEEqFun.mk f hf) p μ = eLpNorm f p μ$$

Lean4

@[simp]
theorem toLp_coeFn (f : Lp E p μ) (hf : MemLp f p μ) : hf.toLp f = f := by simp [MemLp.toLp]

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

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

Разделы

Аффилиация

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