src/HOL/Analysis/Linear_Algebra.thy
 changeset 63886 685fb01256af parent 63881 b746b19197bd child 63918 6bf55e6e0b75
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 15 22:41:05 2016 +0200
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Fri Sep 16 13:56:51 2016 +0200
1.3 @@ -10,6 +10,30 @@
1.4    "~~/src/HOL/Library/Infinite_Set"
1.5  begin
1.6
1.7 +lemma linear_simps:
1.8 +  assumes "bounded_linear f"
1.9 +  shows
1.10 +    "f (a + b) = f a + f b"
1.11 +    "f (a - b) = f a - f b"
1.12 +    "f 0 = 0"
1.13 +    "f (- a) = - f a"
1.14 +    "f (s *\<^sub>R v) = s *\<^sub>R (f v)"
1.15 +proof -
1.16 +  interpret f: bounded_linear f by fact
1.17 +  show "f (a + b) = f a + f b" by (rule f.add)
1.18 +  show "f (a - b) = f a - f b" by (rule f.diff)
1.19 +  show "f 0 = 0" by (rule f.zero)
1.20 +  show "f (- a) = - f a" by (rule f.minus)
1.21 +  show "f (s *\<^sub>R v) = s *\<^sub>R (f v)" by (rule f.scaleR)
1.22 +qed
1.23 +
1.24 +lemma bounded_linearI:
1.25 +  assumes "\<And>x y. f (x + y) = f x + f y"
1.26 +    and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x"
1.27 +    and "\<And>x. norm (f x) \<le> norm x * K"
1.28 +  shows "bounded_linear f"
1.29 +  using assms by (rule bounded_linear_intro) (* FIXME: duplicate *)
1.30 +
1.31  subsection \<open>A generic notion of "hull" (convex, affine, conic hull and closure).\<close>
1.32
1.33  definition hull :: "('a set \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "hull" 75)
```