instCompleteSpace — Mathlib

English

If R is a complete uniform space, then the space of multivariate power series MvPowerSeries σ R is also complete.

Русский

Если R является полным униформ-пространством, то множество mv-рядов MvPowerSeries σ R тоже полностью.

LaTeX

$$CompleteSpace (MvPowerSeries σ R)$$

Lean4

/-- Completeness of the uniform structure on `MvPowerSeries` -/
@[scoped instance]
theorem instCompleteSpace [CompleteSpace R] : CompleteSpace (MvPowerSeries σ R) :=
  Pi.complete _

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