English
Let E be a topological abelian group and F a complete 𝕜‑normed space. Then the space of continuous ι‑variable alternating multilinear maps from E to F (over 𝕜) is a complete normed space (i.e., a Banach space) when endowed with the operator norm.
Русский
Пусть E — топологическая абелова группа, F — полное нормированное по 𝕜 пространство. Тогда пространство непрерывных чередующихся многолинейных отображений из E^ι в F (по 𝕜) является полным нормированным пространством (банаховым) относительно операционного нормирования.
LaTeX
$$$\\text{The space of continuous alternating multilinear maps } E^{\\otimes ι} \\to F \\text{ is complete (a Banach space) provided } F \\text{ is complete and } E \\text{ satisfies the stated topological conditions.}$$$
Lean4
instance instCompleteSpace [IsTopologicalAddGroup E] [SequentialSpace (ι → E)] : CompleteSpace (E [⋀^ι]→L[𝕜] F) :=
completeSpace <| .of_seq fun _u x hux ↦ (hux.isVonNBounded_range 𝕜).insert x
