moved basic theorem
authorimmler
Tue, 27 Aug 2019 16:25:00 +0200
changeset 70801 8b7f6ecb3369
parent 70800 7bf683f3672d
child 70802 60483d0385d6
moved basic theorem
src/HOL/Analysis/Interval_Integral.thy
src/HOL/Deriv.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Tue Aug 27 13:22:33 2019 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Tue Aug 27 16:25:00 2019 +0200
@@ -8,10 +8,6 @@
   imports Equivalence_Lebesgue_Henstock_Integration
 begin
 
-lemma continuous_on_vector_derivative:
-  "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
-  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
-
 definition "einterval a b = {x. a < ereal x \<and> ereal x < b}"
 
 lemma einterval_eq[simp]:
--- a/src/HOL/Deriv.thy	Tue Aug 27 13:22:33 2019 +0200
+++ b/src/HOL/Deriv.thy	Tue Aug 27 16:25:00 2019 +0200
@@ -797,6 +797,10 @@
   "(f has_vector_derivative D) (at x within s) \<Longrightarrow> continuous (at x within s) f"
   by (auto intro: has_derivative_continuous simp: has_vector_derivative_def)
 
+lemma continuous_on_vector_derivative:
+  "(\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)) \<Longrightarrow> continuous_on S f"
+  by (auto simp: continuous_on_eq_continuous_within intro!: has_vector_derivative_continuous)
+
 lemma has_vector_derivative_mult_right[derivative_intros]:
   fixes a :: "'a::real_normed_algebra"
   shows "(f has_vector_derivative x) F \<Longrightarrow> ((\<lambda>x. a * f x) has_vector_derivative (a * x)) F"