instTopologicalSpace — Mathlib

English

The topology on PowerSeries R is the pointwise (Pi) topology, i.e., the product topology given by the coefficient maps.

Русский

Топология на степенных рядах PowerSeries R — точечная (Pi) топология, задаваемая отображениями коэффициентов.

LaTeX

$$$ \\mathcal{T}_{\\PowerSeries(R)} = \\Pi_{d \\in \\mathbb{N}} \\mathcal{T}_R $$$

Lean4

/-- The pointwise topology on `PowerSeries` -/
scoped instance : TopologicalSpace (PowerSeries R) :=
  Pi.topologicalSpace

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