--- a/src/HOL/Real_Vector_Spaces.thy Thu Sep 12 15:08:46 2013 -0700
+++ b/src/HOL/Real_Vector_Spaces.thy Thu Sep 12 18:09:17 2013 -0700
@@ -934,8 +934,16 @@
subsection {* Bounded Linear and Bilinear Operators *}
-locale bounded_linear = additive f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
+locale linear = additive f for f :: "'a::real_vector \<Rightarrow> 'b::real_vector" +
assumes scaleR: "f (scaleR r x) = scaleR r (f x)"
+
+lemma linearI:
+ assumes "\<And>x y. f (x + y) = f x + f y"
+ assumes "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
+ shows "linear f"
+ by default (rule assms)+
+
+locale bounded_linear = linear f for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" +
assumes bounded: "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
begin
@@ -1547,4 +1555,3 @@
qed
end
-