Theorem isIntegralCurveAt_iff_exists_mem_nhds

Modification history

2026-03-20 20:42
Mathlib/Analysis/ODE/Basic.lean
feat: IsIntegralCurve for solutions to ODEs (#29186) …
Added isIntegralCurveAt_iff_exists_mem_nhdsView on Github →