instT0Space

Mathlib.RingTheory.MvPowerSeries.PiTopology

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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