feat(topology): continuous sections of a vector bundle are a vector space

[Nicknamen]

The main idea behind this PR is to implement sections both as bundled right inverses and as dependent type functions, and profit of the benefits of both.

Let E : B → Type* be the collection of fibers of a bundle on B. In the case of sections of bundle we prove that the type of right inverses of bundle.proj E is equivalent to the type Π x : B, E x. Both implementations of sections have their advantages:
right_inv (proj E) is better to talk about properties such as continuity, whereas Π x : B, E x works better with algebraic structures, it naturally inherits the algebraic structures present on the fibers, thanks to the Π instances. It is hence a good idea to implement both and write down the equivalence between them, but then we have to choose only one for our final implementation of sections.

I believe this PR is important to show that the previously given implementation of vector bundles is natural and works well.

---

• depends on: [Merged by Bors] - chore(topology/topological_fiber_bundle): reorganizing the code #7938
• depends on: [Merged by Bors] - refactor(topology/vector_bundle): redefine #13175

[Nicknamen]

@sgouezel sorry why did you change the labels?

[sgouezel]

Because you have made some suggestions on github but you haven't committed them, so I thought you were still updating the PR. It doesn't make sense for us to start reviewing if you are still changing the PR.

[Nicknamen]

Oh I just realized while reading the diff page that I left some typos in the docs, and I registered them as suggestions because I thought I could commit them together with the next easy suggestions that you or other maintainers will make, but if you prefer I can commit my corrections before

[sgouezel]

Yes, please do commit them: it means that there are less discussions open, so we can focus on the interesting ones, and also when we look at the files we won't be disturbed by the typos.

[Nicknamen]

Done

[leanprover-community-bot-assistant]

This PR/issue depends on:

• [Merged by Bors] - chore(topology/topological_fiber_bundle): reorganizing the code #7938
• [Merged by Bors] - refactor(topology/vector_bundle): redefine #13175
  By Dependent Issues (🤖). Happy coding!

[sgouezel]

Can you merge master and fix the build?

[Nicknamen]

Lean is weirdly not letting me open the namespace trivialization... but apart from that things work smoothly

[hrmacbeth]

I think, with this PR, the time has come to make a topology/vector_bundle/ folder. Could you do that with this PR, putting your material in a new file, and maybe also splitting out the direct sum construction?

[Nicknamen]

Should we make a folder bundle where to put also fiber bundles and, in the future, principal bundles? Or just a folder for vector bundles?

[joneugster]

I believe most of this PR has been added to master meanwhile. The only thing I couldn't see is the part about sections. (Merged master and left these parts about sections in for reference). I don't know much, should this be closed, or is that part about sections something you would want to add still?