theorem BoundedOperators.bounded_operators_completeSpace (𝕜 : Type u_1) (V : Type u_2) (W : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [NormedAddCommGroup W] [NormedSpace 𝕜 W] [CompleteSpace W] : CompleteSpace (V →L[𝕜] W)

If $V$ is a normed vector space over a nontrivially normed field $𝕜$ and $W$ is a Banach space (a complete normed $𝕜$-vector space), then the space of bounded linear operators $\mathcal{B}(V, W) = V \to_L[𝕜] W$ is itself a Banach space, i.e., it is complete with respect to the operator norm.