instTopologicalSpace — Mathlib

English

The Schwartz space is endowed with a natural topology coming from its family of seminorms.

Русский

Schwartz-пространство снабжено естественной топологией, полученной из семейства семинорм.

LaTeX

$$$\text{instTopologicalSpace} : TopologicalSpace\; \mathcal{S}(E,F)$$$

Lean4

instance instTopologicalSpace : TopologicalSpace 𝓢(E, F) :=
  (schwartzSeminormFamily ℝ E F).moduleFilterBasis.topology'

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