instT2Space

Mathlib.RingTheory.MvPowerSeries.PiTopology

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.WithPiTopology.instT2Space

← MathLib Explorer

English

If R is a T2 space, then the mv power series space is T2.

Русский

Если R является T2-пространством, то и пространство MvPowerSeries σ R является T2.

LaTeX

$$[T2Space R] ⇒ T2Space (MvPowerSeries σ R)$$

Lean4

/-- `MvPowerSeries` on a `T2Space` form a `T2Space` -/
@[scoped instance]
theorem instT2Space [T2Space R] : T2Space (MvPowerSeries σ R) :=
  Pi.t2Space

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

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

Разделы

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

Аффилиация

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