memℓp

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#lp.memℓp

English

Protected theorem memℓp: for f in lp, Memℓp f p holds.

Русский

Защищённая теорема memℓp: для f ∈ lp верно Memℓp f p.

LaTeX

$$$$ \mathrm{Mem}_{\ell^p}(f,p) = f.prop. $$$$

Lean4

protected theorem memℓp (f : lp E p) : Memℓp f p :=
  f.prop

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

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

Разделы

Аффилиация

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