Theorem isIntegralCurveOn_iff_isIntegralCurveAt

Modification history

2026-03-20 20:42
Mathlib/Analysis/ODE/Basic.lean
feat: IsIntegralCurve for solutions to ODEs (#29186) …
Added isIntegralCurveOn_iff_isIntegralCurveAtView on Github →
2025-08-13 22:41
Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
chore: rename `IsIntegralCurve` to `IsMIntegralCurve` (#26563) …
Deleted isIntegralCurveOn_iff_isIntegralCurveAtView on Github →
2024-11-12 02:53
Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
chore: split `IntegralCurve` (#18833) …
Modified isIntegralCurveOn_iff_isIntegralCurveAtView on Github →
2024-01-09 02:13
Mathlib/Geometry/Manifold/IntegralCurve.lean
feat: local existence of integral curves of vector field (#8483) …
Added isIntegralCurveOn_iff_isIntegralCurveAtView on Github →