instT0Space

Mathlib.RingTheory.PowerSeries.PiTopology

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

← MathLib Explorer

English

If R is a T0 space, then PowerSeries(R) is also a T0 space.

Русский

Если R является T0-пространством, то и PowerSeries(R) является T0-пространством.

LaTeX

$$$ \\text{T0Space}(R) \\implies \\text{T0Space}(\\PowerSeries(R)) $$$

Lean4

/-- Separation of the topology on `PowerSeries` -/
@[scoped instance]
theorem instT0Space [T0Space R] : T0Space (PowerSeries R) :=
  MvPowerSeries.WithPiTopology.instT0Space

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

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

Разделы

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

Аффилиация

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