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)