summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Real/HahnBanach/Linearform.thy

changeset 27612 | d3eb431db035 |

parent 27611 | 2c01c0bdb385 |

child 29234 | 60f7fb56f8cd |

1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 16:50:09 2008 +0200 1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 19:39:37 2008 +0200 1.3 @@ -5,7 +5,9 @@ 1.4 1.5 header {* Linearforms *} 1.6 1.7 -theory Linearform imports VectorSpace begin 1.8 +theory Linearform 1.9 +imports VectorSpace 1.10 +begin 1.11 1.12 text {* 1.13 A \emph{linear form} is a function on a vector space into the reals 1.14 @@ -25,9 +27,9 @@ 1.15 proof - 1.16 interpret vectorspace [V] by fact 1.17 assume x: "x \<in> V" 1.18 - hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1) 1.19 - also from x have "... = (- 1) * (f x)" by (rule mult) 1.20 - also from x have "... = - (f x)" by simp 1.21 + then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1) 1.22 + also from x have "\<dots> = (- 1) * (f x)" by (rule mult) 1.23 + also from x have "\<dots> = - (f x)" by simp 1.24 finally show ?thesis . 1.25 qed 1.26 1.27 @@ -37,8 +39,8 @@ 1.28 proof - 1.29 interpret vectorspace [V] by fact 1.30 assume x: "x \<in> V" and y: "y \<in> V" 1.31 - hence "x - y = x + - y" by (rule diff_eq1) 1.32 - also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y) 1.33 + then have "x - y = x + - y" by (rule diff_eq1) 1.34 + also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y) 1.35 also have "f (- y) = - f y" using `vectorspace V` y by (rule neg) 1.36 finally show ?thesis by simp 1.37 qed