instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal

Mathlib.Analysis.CStarAlgebra.lpSpace

URI: https://scilib.ai/kg/mathlib#instNonUnitalCommCStarAlgebraSubtypePreLpMemAddSubgroupLpTopENNReal

Lean4

instance [∀ i, NonUnitalCommCStarAlgebra (A i)] : NonUnitalCommCStarAlgebra (lp A ∞) where
  -- it's slightly weird that we need the `Nontrivial` instance here
  -- it's because we have no way to say that `‖(1 : A i)‖` is uniformly bounded as a type class
  -- aside from `∀ i, NormOneClass (A i)`, this holds automatically for C⋆-algebras though.

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

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

Разделы

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

Аффилиация

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