Sebastien Gouezel

Results 27 comments of Sebastien Gouezel

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

> Secondly, I am not sure what you mean with "more important": operations fiberwise are easy to deal with whereas the real hard part when it comes to sections is...

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

Any of them that you'd like to bundle.

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

I am pretty sure all these should be unbundled, yes.

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

Let's first do it in coordinate charts. A vector field is a function `E -> E`. The derivative of a function with respect to a vector field is `fderiv_at f...

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

> > > Before you wrote > > > My question is not so much with definitions than with theorems: as things are currently written you don't prove that if...

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

> > > I am not sure I understand this sentence: > > > In manifolds, a vector field is a section of the tangent bundle > > How do...

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

If I remember correctly, we agreed that the right setting for our bundles is Pi types. So I don't see the relevance of the file `data/right_inv` for this PR. Also,...