zero_mem_ℓp'

Mathlib.Analysis.Normed.Lp.lpSpace

URI: https://scilib.ai/kg/mathlib#zero_mem_ℓp'

English

The constant-zero family is in ℓp for any p.

Русский

Постоянно нулевые значения образуют элемент ℓ^p для любого p.

LaTeX

$$$$ \mathrm{Mem}_{\ell^p}(0,p). $$$$

Lean4

theorem zero_mem_ℓp' : Memℓp (fun i : α => (0 : E i)) p :=
  zero_memℓp

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

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

Разделы

Аффилиация

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