instT2Space

Mathlib.RingTheory.PowerSeries.PiTopology

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

← MathLib Explorer

English

If R is a T2 space, then PowerSeries(R) is a T2 space.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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