author immler 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 file | annotate | diff | comparison | revisions src/HOL/Deriv.thy file | annotate | diff | comparison | revisions
```--- 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"```