equal
deleted
inserted
replaced
175 have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)" |
175 have "FDERIV (\<lambda>x. 0) x :> (\<lambda>h. F h - F' h)" |
176 using FDERIV_diff [OF assms] by simp |
176 using FDERIV_diff [OF assms] by simp |
177 hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)" |
177 hence "(\<lambda>h. F h - F' h) = (\<lambda>h. 0)" |
178 by (rule FDERIV_zero_unique) |
178 by (rule FDERIV_zero_unique) |
179 thus "F = F'" |
179 thus "F = F'" |
180 unfolding expand_fun_eq right_minus_eq . |
180 unfolding ext_iff right_minus_eq . |
181 qed |
181 qed |
182 |
182 |
183 subsection {* Continuity *} |
183 subsection {* Continuity *} |
184 |
184 |
185 lemma FDERIV_isCont: |
185 lemma FDERIV_isCont: |