Commit 2024-11-27 13:34 37c90e46

feat: uniform time lemma for the existence of global integral curves (#9013) Lemma 9.15 in Lee's Introduction to Smooth Manifolds:

Let v be a smooth vector field on a smooth manifold M. If there exists ε > 0 such that for each point x : M, there exists an integral curve of v through x defined on an open interval Ioo (-ε) ε, then every point on M has a global integral curve of v passing through it. We only require v to be $C^1$. To achieve this, we define the extension of an integral curve γ by another integral curve γ', if they agree at a point inside their overlapping open interval domains. This utilises the uniqueness theorem of integral curves. We need this lemma to show that vector fields on compact manifolds always have global integral curves.

• depends on: #8886
• depends on: #18833
• depends on: #19008