`BookProof.Howland.hasDerivAt_autonomize` (f : ℝ → E → E) (x : ℝ → E) (t : ℝ) (hx : HasDerivAt x (f t (x t)) t) : HasDerivAt (fun s : ℝ => ((s, x s) : ℝ × E)) (autonomize f (t, x t

Initializing...

`BookProof.Howland.hasDerivAt_autonomize` (f : ℝ → E → E) (x : ℝ → E) (t : ℝ) (hx : HasDerivAt x (f t (x t)) t) : HasDerivAt (fun s : ℝ => ((s, x s) : ℝ × E)) (autonomize f (t, x t · Prove2Me