isEmbedding_restrictScalars — Mathlib

English

The map restrictScalars 𝕜' is continuous between the spaces of multilinear maps when endowed with the natural topologies.

Русский

Отображение restrictScalars 𝕜' непрерывно между соответствующими пространствами много-линейных отображений с естественными топологиями.

LaTeX

$$$\\text{Continuous}(\\mathrm{restrictScalars}\\, 𝕜')$$$

Lean4

theorem isEmbedding_restrictScalars :
    IsEmbedding (restrictScalars 𝕜' : ContinuousMultilinearMap 𝕜 E F → ContinuousMultilinearMap 𝕜' E F) :=
  letI : UniformSpace F := IsTopologicalAddGroup.toUniformSpace F
  haveI : IsUniformAddGroup F := isUniformAddGroup_of_addCommGroup
  (isUniformEmbedding_restrictScalars _).isEmbedding

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