Commit 2024-11-19 00:27 812897a4
View on Github →feat(Manifold/IntegralCurve/Transform): pointwise notation and translation 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).