feat(topology/algebra/module/strong_operator, analysis/normed_space/operator_norm): strong operator topology

[ADedecker]

trafficstars

---

• [ ] depends on: #14857
• [ ] depends on: #16052
• [ ] depends on: #16054

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• leanprover-community/mathlib#14857
• ~~leanprover-community/mathlib#16052~~
• ~~leanprover-community/mathlib#16054~~ By Dependent Issues (🤖). Happy coding!

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#14857~~
• ~~leanprover-community/mathlib#16052~~
• ~~leanprover-community/mathlib#16054~~ By Dependent Issues (🤖). Happy coding!

[ADedecker]

I guess it would be nice to see the topology in action

Is there anything in particular you'd like to have? I must say this has been waiting for so long I don't have a clear idea of what I wanted to do next. Everything is in place to show that precomposition and postcomposition by fixed continuous linear maps are continuous (so in particular the transpose of a continuous linear map is still continuous), which is one of the main things you need for distributions I think, but if you need anything feel free to ask for it :)

[mcdoll]

I was thinking about something like the characterization of convergence of distributions in a with_seminorm p space, but as I've said the PR is long enough already.

[mcdoll]

Since there have been no further comments for a week, I think we should merge it.

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by mcdoll.

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests