Commit 2025-07-01 21:41 3fdfb240

View on Github →

feat: fix definition of IsIntegralCurveOn for consistency (#26533) I change the definition of IsIntegralCurveOn to use HasMFDerivWithinAt, rather than HasMFDerivAt, so as to make this definition consistent with DifferentiableOn and ContinuousOn. While the API around it slightly changes, there is no effect on the statement of any downstream lemmas.

Estimated changes

Modified Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean

deleted theorem IsIntegralCurveOn.continuousAt

added theorem IsIntegralCurveOn.continuousWithinAt

deleted theorem IsIntegralCurveOn.hasDerivAt

added theorem IsIntegralCurveOn.hasDerivWithinAt

deleted theorem IsIntegralCurveOn.of_union

Modified Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve/Transform.lean

Modified Mathlib/Geometry/Manifold/IntegralCurve/UniformTime.lean