src/HOL/Multivariate_Analysis/Derivative.thy
 changeset 51733 70abecafe9ac parent 51642 400ec5ae7f8f child 53077 a1b3784f8129
equal inserted replaced
51732:4392eb046a97 51733:70abecafe9ac
`  1431     by (rule frechet_derivative_unique_at)`
`  1431     by (rule frechet_derivative_unique_at)`
`  1432   thus ?thesis unfolding fun_eq_iff by auto`
`  1432   thus ?thesis unfolding fun_eq_iff by auto`
`  1433 qed`
`  1433 qed`
`  1434 `
`  1434 `
`  1435 lemma vector_derivative_unique_within_closed_interval:`
`  1435 lemma vector_derivative_unique_within_closed_interval:`
`  1437   assumes "a < b" and "x \<in> {a..b}"`
`  1436   assumes "a < b" and "x \<in> {a..b}"`
`  1438   assumes "(f has_vector_derivative f') (at x within {a..b})"`
`  1437   assumes "(f has_vector_derivative f') (at x within {a..b})"`
`  1439   assumes "(f has_vector_derivative f'') (at x within {a..b})"`
`  1438   assumes "(f has_vector_derivative f'') (at x within {a..b})"`
`  1440   shows "f' = f''"`
`  1439   shows "f' = f''"`
`  1441 proof-`
`  1440 proof-`
`  1458   apply(rule vector_derivative_unique_at) defer apply assumption`
`  1457   apply(rule vector_derivative_unique_at) defer apply assumption`
`  1459   unfolding vector_derivative_works[THEN sym] differentiable_def`
`  1458   unfolding vector_derivative_works[THEN sym] differentiable_def`
`  1460   unfolding has_vector_derivative_def by auto`
`  1459   unfolding has_vector_derivative_def by auto`
`  1461 `
`  1460 `
`  1462 lemma vector_derivative_within_closed_interval:`
`  1461 lemma vector_derivative_within_closed_interval:`
`  1464   assumes "a < b" and "x \<in> {a..b}"`
`  1462   assumes "a < b" and "x \<in> {a..b}"`
`  1465   assumes "(f has_vector_derivative f') (at x within {a..b})"`
`  1463   assumes "(f has_vector_derivative f') (at x within {a..b})"`
`  1466   shows "vector_derivative f (at x within {a..b}) = f'"`
`  1464   shows "vector_derivative f (at x within {a..b}) = f'"`
`  1467   apply(rule vector_derivative_unique_within_closed_interval)`
`  1465   apply(rule vector_derivative_unique_within_closed_interval)`
`  1468   using vector_derivative_works[unfolded differentiable_def]`
`  1466   using vector_derivative_works[unfolded differentiable_def]`