instUniformSpace — Mathlib

English

The topology on ContinuousMultilinearMap 𝕜 E F is the induced topology from the UniformOnFun topology on the space of uniform-on-fun maps.

Русский

Топология на ContinuousMultilinearMap 𝕜 E F есть индуцированная от топологии UniformOnFun на пространстве uniform-on-fun отображений.

LaTeX

$$$\text{TopologicalSpace}(\text{ContinuousMultilinearMap }\mathcal{M}) = \text{induced}\left(\text{toUniformOnFun}, \text{UniformOnFun.topologicalSpace}\right)$$$

Lean4

instance instUniformSpace [UniformSpace F] [IsUniformAddGroup F] : UniformSpace (ContinuousMultilinearMap 𝕜 E F) :=
  .replaceTopology (.comap toUniformOnFun <| UniformOnFun.uniformSpace _ _ _) <| by
    rw [instTopologicalSpace, IsUniformAddGroup.toUniformSpace_eq]; rfl

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