const_mem_Lp

Mathlib.MeasureTheory.Function.LpSpace.Basic

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

← MathLib Explorer

English

If μ is finite and c ∈ E, then the constant function c belongs to Lp(E, p, μ).

Русский

Если мера μ конечна и c ∈ E, то константная функция c принадлежит Lp(E, p, μ).

LaTeX

$$c ∈ L_p(E,p,\mu)$$

Lean4

theorem const_mem_Lp (α) {_ : MeasurableSpace α} (μ : Measure α) (c : E) [IsFiniteMeasure μ] :
    @AEEqFun.const α _ _ μ _ c ∈ Lp E p μ :=
  (memLp_const c).eLpNorm_mk_lt_top

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

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

Разделы

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

Аффилиация

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