memLp_const

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.memLp_const

English

Same as above, reiterating that a constant with finite EN-norm yields MemLp under finite measure.

Русский

Повторение: константа с конечной EN-нормой принадлежит MemLp при конечной мере.

LaTeX

$$MemLp (fun _ : α => c) p μ$$

Lean4

theorem memLp_const (c : E) [IsFiniteMeasure μ] : MemLp (fun _ : α => c) p μ :=
  memLp_const_enorm enorm_ne_top

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

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

Разделы

Аффилиация

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