# [isabelle] Mean value theorem for has_vector_derivative

Hi,

`For a step of a proof I'm working on I'd like to use "âjâ{a .. b}. âlâ{j
``.. b}. G j â G l" where G has derivative g â 0. The standard way to
``prove this is using the mean value theorem which already exists in the
``MVA/Derivative theory.
``Unfortunately the mvt is formulated for has_derivative and I have to use
``G has_vector_derivative g rather than has_derivative as G is defined to
``be (%y. LBINT x=a..y. g x) and using has_derivative leads to a type
``error ereal/real_normed_vector.
``Should I just go back and prove the MVT for has_vector_derivative or is
``there an easier way around this?
`
Cheers,
Alex Hicks

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*