…ation lemmas for subtraction (#19008)

We restate the translation lemmas for integral curves using the `Pointwise` API and add translation lemmas for subtraction for convenience.

This is just split out from #9013.

The `Pointwise` API allows us to use lemmas like `Metric.vadd_ball` and more convenient rewriting of the `dt` term (rather than rewriting it inside the set builder notation).

…ation lemmas for subtraction (#19008)

We restate the translation lemmas for integral curves using the `Pointwise` API and add translation lemmas for subtraction for convenience.

This is just split out from #9013.

The `Pointwise` API allows us to use lemmas like `Metric.vadd_ball` and more convenient rewriting of the `dt` term (rather than rewriting it inside the set builder notation).

…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.

- [x] depends on: #8886 
- [x] depends on: #18833
- [x] depends on: #19008



Co-authored-by: Michael Rothgang <rothgang@math.uni-bonn.de>
Co-authored-by: Johan Commelin <johan@commelin.net>