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.9    using fst_add fst_scaleR
    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.14    using snd_add snd_scaleR
    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)"