isClosedEmbedding_toContinuousMultilinearMap

English

If F is a T2 space, the natural map from the space of alternating continuous maps to the corresponding continuous multilinear maps is a closed embedding.

Русский

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

LaTeX

$$$\\text{IsClosedEmbedding}(\\text{toContinuousMultilinearMap})$$$

Lean4

theorem isClosedEmbedding_toContinuousMultilinearMap [T2Space F] :
    IsClosedEmbedding (toContinuousMultilinearMap : (E [⋀^ι]→L[𝕜] F) → ContinuousMultilinearMap 𝕜 (fun _ : ι ↦ E) F) :=
  ⟨isEmbedding_toContinuousMultilinearMap, isClosed_range_toContinuousMultilinearMap⟩

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