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
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)] :
If a space of linear maps from E to F is complete, and E is nontrivial, then F is
complete.
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] :
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) :
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.
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) :