instProdT0Space

Mathlib.Analysis.Normed.Lp.ProdLp

URI: https://scilib.ai/kg/mathlib#WithLp.instProdT0Space

English

If α and β are T0 spaces, then WithLp p (α × β) is a T0-space.

Русский

Если пространства α и β — T0, то WithLp p (α × β) является T0-пространством.

LaTeX

$$$$\text{WithLp.instProdT0Space }(p, α, β) : T0\text{Space}(WithLp p (α × β))$$$$

Lean4

instance instProdT0Space : T0Space (WithLp p (α × β)) :=
  Prod.instT0Space

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

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

Разделы

Аффилиация

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