completeSpace

Mathlib.Analysis.Normed.Lp.PiLp

URI: https://scilib.ai/kg/mathlib#PiLp.completeSpace

← MathLib Explorer

English

If each β_i is a complete space, then the PiLp p β space is complete.

Русский

Если каждое β_i полно в пространстве, то PiLp p β полно.

LaTeX

$$CompleteSpace (PiLp p β)$$

Lean4

instance completeSpace [∀ i, UniformSpace (β i)] [∀ i, CompleteSpace (β i)] : CompleteSpace (PiLp p β) :=
  inferInstanceAs <| CompleteSpace (Π i, β i)

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

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

Разделы

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

Аффилиация

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