isEmbedding_toContinuousMultilinearMap

English

The canonical injection from the space of continuous alternating multilinear maps into the space of all continuous multilinear maps is an embedding.

Русский

Каноническое включение пространства непрерывных чередующихся мультиляйнерных отображений в пространство всех непрерывных мультиляйнерных отображений является вложением.

LaTeX

$$$\\text{toContinuousMultilinearMap}: \\text{Alt}^ι(E;F) \\hookrightarrow \\text{CLM}_{𝕜}(E;F)$ is an embedding$$

Lean4

theorem isEmbedding_toContinuousMultilinearMap : IsEmbedding (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F → _)) :=
  letI := IsTopologicalAddGroup.toUniformSpace F
  haveI := isUniformAddGroup_of_addCommGroup (G := F)
  isUniformEmbedding_toContinuousMultilinearMap.isEmbedding

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