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)
: