instUniformSpace — Mathlib

English

Uniform structure on SchwartzMap is compatible with the module structure and the scalar action.

Русский

Единая структура SchwartzMap согласована с модульной структурой и действием скаляров.

LaTeX

$$$\text{instUniformSpace}$ is compatible with $\text{instModule}$ and scalar action$$

Lean4

instance instUniformSpace : UniformSpace 𝓢(E, F) :=
  (schwartzSeminormFamily ℝ E F).addGroupFilterBasis.uniformSpace

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