Commit 2024-07-21 01:25 c8f5845f

feat: define the weak operator topology (#14177) This PR defines the weak operator topology on maps between normed spaces and proves some of its basic properties. It creates a type copy of E →L[𝕜] F endowed with the WOT rather than the norm topology. Along the way, we define several lemmas that are useful for proving properties of a topology that is induced by a bundled hom. Note: I've defined the global notation E →WOT[𝕜] F for the type copy; I don't think this is likely to collide with anything else, but I can make it scoped if this is deemed preferable.