# Completeness of spaces of linear and multilinear maps #

If `E` is a nontrivial normed space over a nontrivially normed field `𝕜`, and `E` has a separating dual, then for any normed space `F`, the completeness of the space of continuous linear maps from `E` to `F` is equivalent to the completeness of `F`.

A similar statement holds for spaces of continuous multilinear maps

source
theorem SeparatingDual.completeSpace_of_completeSpace_continuousLinearMap (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [SeparatingDual 𝕜 E] [Nontrivial E] [CompleteSpace (E →L[𝕜] F)] :
CompleteSpace F

If a space of linear maps from `E` to `F` is complete, and `E` is nontrivial, then `F` is complete.

source
theorem SeparatingDual.completeSpace_continuousLinearMap_iff (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [SeparatingDual 𝕜 E] [Nontrivial E] :
CompleteSpace (E →L[𝕜] F) ↔ CompleteSpace F
source
theorem SeparatingDual.completeSpace_of_completeSpace_continuousMultilinearMap (𝕜 : Type u_1) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_4} [Finite ι] {M : ι → Type u_5} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] [∀ (i : ι), SeparatingDual 𝕜 (M i)] [CompleteSpace (ContinuousMultilinearMap 𝕜 M F)] {m : (i : ι) → M i} (hm : ∀ (i : ι), m i ≠ 0) :
CompleteSpace F

If a space of multilinear maps from `Π i, E i` to `F` is complete, and each `E i` has a nonzero element, then `F` is complete.

source
theorem SeparatingDual.completeSpace_continuousMultilinearMap_iff (𝕜 : Type u_1) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {ι : Type u_4} [Finite ι] {M : ι → Type u_5} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] [∀ (i : ι), SeparatingDual 𝕜 (M i)] {m : (i : ι) → M i} (hm : ∀ (i : ι), m i ≠ 0) :
CompleteSpace (ContinuousMultilinearMap 𝕜 M F) ↔ CompleteSpace F