src/HOL/Analysis/Product_Vector.thy
 changeset 68607 67bb59e49834 parent 68072 493b818e8e10 child 68611 4bc4b5c0ccfc
```     1.1 --- a/src/HOL/Analysis/Product_Vector.thy	Mon Jul 09 21:55:40 2018 +0100
1.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Tue Jul 10 09:38:35 2018 +0200
1.3 @@ -314,11 +314,11 @@
1.4
1.5  subsubsection%unimportant \<open>Pair operations are linear\<close>
1.6
1.7 -lemma%important bounded_linear_fst: "bounded_linear fst"
1.8 +proposition bounded_linear_fst: "bounded_linear fst"
1.10    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
1.11
1.12 -lemma%important bounded_linear_snd: "bounded_linear snd"
1.13 +proposition bounded_linear_snd: "bounded_linear snd"
1.15    by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def)
1.16
1.17 @@ -354,10 +354,10 @@
1.18
1.19  subsubsection%unimportant \<open>Frechet derivatives involving pairs\<close>
1.20
1.21 -lemma%important has_derivative_Pair [derivative_intros]:
1.22 +proposition has_derivative_Pair [derivative_intros]:
1.23    assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
1.24    shows "((\<lambda>x. (f x, g x)) has_derivative (\<lambda>h. (f' h, g' h))) (at x within s)"
1.25 -proof%unimportant (rule has_derivativeI_sandwich[of 1])
1.26 +proof (rule has_derivativeI_sandwich[of 1])
1.27    show "bounded_linear (\<lambda>h. (f' h, g' h))"
1.28      using f g by (intro bounded_linear_Pair has_derivative_bounded_linear)
1.29    let ?Rf = "\<lambda>y. f y - f x - f' (y - x)"
```