src/HOL/Real_Vector_Spaces.thy
changeset 53600 8fda7ad57466
parent 53381 355a4cac5440
child 54230 b1d955791529
     1.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Sep 12 15:08:46 2013 -0700
     1.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Thu Sep 12 18:09:17 2013 -0700
     1.3 @@ -934,8 +934,16 @@
     1.4  
     1.5  subsection {* Bounded Linear and Bilinear Operators *}
     1.6  
     1.7 -locale bounded_linear = additive f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
     1.8 +locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
     1.9    assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
    1.10 +
    1.11 +lemma linearI:
    1.12 +  assumes "\<And>x y. f (x + y) = f x + f y"
    1.13 +  assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
    1.14 +  shows "linear f"
    1.15 +  by default (rule assms)+
    1.16 +
    1.17 +locale bounded_linear = linear f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
    1.18    assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
    1.19  begin
    1.20  
    1.21 @@ -1547,4 +1555,3 @@
    1.22  qed
    1.23  
    1.24  end
    1.25 -