Smooth dependence of initial conditions

Stream: Is there code for X?

[Michael Rothgang]

Mathlib does have the existence and uniqueness theorems for ODEs (say, with a Lipschitz condition). Is the smooth dependence on the initial conditions already in mathlib?

(This came up in #9013, when discussing "easy" corollaries.)