[Merged by Bors] - feat(analysis/normed_space): Geometric Hahn Banach theorems

[b-mehta]

This proves a range of variants of the Hahn-Banach separation theorems.

---

• depends on: [Merged by Bors] - feat(analysis/seminorm): define the Minkowski functional #9097
• depends on: [Merged by Bors] - feat(analysis/convex/topology): Separating by convex sets #11458
• depends on: [Merged by Bors] - feat(analysis/seminorm): The norm as a seminorm, balanced and absorbent lemmas #11487
• depends on: [Merged by Bors] - feat(topology/algebra/module/basic): A continuous linear functional is open #13829
• depends on: [Merged by Bors] - feat(analysis/convex/*): Convexity and subtraction #14015
• depends on: [Merged by Bors] - feat(topology/algebra/group): Division is an open map #14028
• depends on: [Merged by Bors] - feat(linear_algebra/linear_pmap): mk_span_singleton of the same point #14029
• depends on: [Merged by Bors] - feat({data/{finset,set},order/filter}/pointwise): More lemmas #14216

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(analysis/seminorm): define the Minkowski functional #9097
• [Merged by Bors] - feat(analysis/convex/topology): Separating by convex sets #11458
• [Merged by Bors] - feat(analysis/seminorm): The norm as a seminorm, balanced and absorbent lemmas #11487
• [Merged by Bors] - feat(topology/algebra/module/basic): A continuous linear functional is open #13829
• [Merged by Bors] - feat(analysis/convex/*): Convexity and subtraction #14015
• [Merged by Bors] - feat(topology/algebra/group): Division is an open map #14028
• [Merged by Bors] - feat(linear_algebra/linear_pmap): mk_span_singleton of the same point #14029
• [Merged by Bors] - feat({data/{finset,set},order/filter}/pointwise): More lemmas #14216
  By Dependent Issues (🤖). Happy coding!

[hrmacbeth]

bors r+

Thanks! This ended up being quite a good test for the convexity library :)

[YaelDillies]

Indeed! This has been a long year of continuous additions to convexity. I will make a tree of PR dependencies to celebrate 🥳

[b-mehta]

Really happy to see this merged! Thanks @YaelDillies for your determined efforts on this and for cleaning up some of my mess, and thanks @hrmacbeth and all the other reviewers for helping make this the best it can be!

[bors]

Pull request successfully merged into master.

Build succeeded:

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