Genuine closed-interval derivatives lift through injective bounded embeddings.

theorem EulerInjectivePathDerivative.hasDerivWithinAt_of_injective_map {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (L : E →L[ℝ] F) (hL : Function.Injective ⇑L) (T : ℝ) (hT : 0 ≤ T) (u f : C(↑(Set.Icc 0 T), E)) (hd : ∀ t ∈ Set.Ioo 0 T, HasDerivAt (fun (r : ℝ) => L (EulerVolterraConvolution.extendPath T hT u r)) (L (EulerVolterraConvolution.extendPath T hT f t)) t) (t : ↑(Set.Icc 0 T)) : HasDerivWithinAt (EulerVolterraConvolution.extendPath T hT u) (f t) (Set.Icc 0 T) ↑t

A continuous stronger-space derivative is genuine even at the interval endpoints.