feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces

[ADedecker]

---

• [ ] depends on: #16782
• [ ] depends on: #16749

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#16782~~
• ~~leanprover-community/mathlib#16749~~ By Dependent Issues (🤖). Happy coding!

[ADedecker]

About moving files: everything in hahn_banach/separation now works in any locally convex space, so we just have to discuss moving the full file. I'd argue that we definitely want to keep the two hahn_banach files together. Eventually we'll want to move the whole hahn_banach folder to analysis/locally_convex, so I guess it is just a matter of doing now or postponing it to when the extension file is generalized too. Both options are fine to me, but again I don't want to move one file and not the other. For Krein-Milman I don't have a strong opinion, but keeping it in analysis/convex definitely doesn't feel wrong since it's primarily a geometric statement.

[mcdoll]

I guess we want to keep some of theorems in hahn_banach/extension with the norm as corollaries. I have no strong opinion on when to move the things, if you do it later that is fine with me. The correct place for Krein-Milman is debatable and probably not too important, so let's leave it where it is.

[ADedecker]

Let's leave it there for now then.

[YaelDillies]

I'm happy with moving stuff around but yeah that probably should be a separate PR.

[mcdoll]

Thanks.

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