Integral curves on manifolds

Stream: PR reviews

[Winston Yin (尹維晨)]

Freshly baked and ready for review:

• #8483 proves the local existence of integral curves for tangent vector fields on manifolds
• #8624 defines the interior and boundary points of a manifold (by @Michael Rothgang)
• #8672 defines tangentCoordChange, an abbreviation of VectorBundleCore.coordChange for tangentBundleCore

The first PR depends on the latter two.

[Michael Rothgang]

I've looked at both PRs (which are not mine) and think they're basically ready to go. I don't have review rights - somebody else also needs to approve :-)

[Scott Morrison]

@Michael Rothgang, while someone else has to do the maintainer merge or bors merge command, you can see leave an "approve" review, which will display your name with a green check mark saying that you have approved. This information is very helpful to the "official" reviewers.

[Michael Rothgang]

I know :-)
Let me clarify: I have approved #8672 already (the other PR is still waiting on its dependents).

[Winston Yin (尹維晨)]

A series of PRs about integral curves that I've polished to the extent I can (nested to indicate dependency):

• #9013 uniform time lemma for the existence of global integral curves
  • #8886 uniqueness of local integral curves
    • #9066 <--- why is bors stuck on this one?
    • #8483 existence of local integral curves
      • #8624 interior and boundary of a manifold (by Michael Rothgang)
      • #8672 introduce tangentCoordChange to make coordinate changes on the tangent space less tedious

Any comments, detailed reviews, and golf attempts welcome!

[Winston Yin (尹維晨)]

Also if there are suggestions for how to split these PRs into smaller ones that can be reviewed sooner...

[Scott Morrison]

Not sure why bors hasn't either tried again or reported failure on #9066. I would suggest just merge master, and say bors merge again.

[Winston Yin (尹維晨)]

Added three more PRs:

• #9323 adds a new class for boundaryless manifolds (more general than boundaryless models)
• #9341 naturality of integral curves
• #9343 integral curves are either injective or periodic

Is there somebody I should ask to review these (and previous) PRs? I would love to help develop this part of the library further.

[Oliver Nash]

Thank you for all your work on this. I'll try to find time to review these over the next few days.