instIsTopologicalAddGroup — Mathlib

English

SchwartzMap carries a natural uniform space structure induced by its seminorms.

Русский

SchwartzMap обладает естественным равномеренным пространством, индуцируемым его семинормами.

LaTeX

$$$\mathrm{instUniformSpace}: UniformSpace 𝓢(E,F)$$$

Lean4

instance instIsTopologicalAddGroup : IsTopologicalAddGroup 𝓢(E, F) :=
  (schwartzSeminormFamily ℝ E F).addGroupFilterBasis.isTopologicalAddGroup

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