CompleteSpace (E →SL[σ] F)

Stream: maths

[Yury G. Kudryashov]

In #17244 I'm generalizing CompleteSpace instance for ContinuousLinearMaps from NormedSpaces to TVS. I'm also removing the unneeded T2Space assumption for ContinuousMultilinearMaps and ContinuousAlternatingMaps.
The theorems still require that the topology on the domain is generated by its restrictions to von Neumann bounded sets (+ an instance for the case of a SequentialSpace). Is there a counterexample for some very bad domain TVS?