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

src/HOL/Real/HahnBanach/Linearform.thy

changeset 13547 | bf399f3bd7dc |

parent 13515 | a6a7025fd7e8 |

child 14254 | 342634f38451 |

1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy Thu Aug 29 11:15:36 2002 +0200 1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Thu Aug 29 16:08:30 2002 +0200 1.3 @@ -16,11 +16,9 @@ 1.4 assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y" 1.5 and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x" 1.6 1.7 -locale (open) vectorspace_linearform = 1.8 - vectorspace + linearform 1.9 - 1.10 -lemma (in vectorspace_linearform) neg [iff]: 1.11 - "x \<in> V \<Longrightarrow> f (- x) = - f x" 1.12 +lemma (in linearform) neg [iff]: 1.13 + includes vectorspace 1.14 + shows "x \<in> V \<Longrightarrow> f (- x) = - f x" 1.15 proof - 1.16 assume x: "x \<in> V" 1.17 hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1) 1.18 @@ -29,21 +27,22 @@ 1.19 finally show ?thesis . 1.20 qed 1.21 1.22 -lemma (in vectorspace_linearform) diff [iff]: 1.23 - "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y" 1.24 +lemma (in linearform) diff [iff]: 1.25 + includes vectorspace 1.26 + shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y" 1.27 proof - 1.28 assume x: "x \<in> V" and y: "y \<in> V" 1.29 hence "x - y = x + - y" by (rule diff_eq1) 1.30 - also have "f ... = f x + f (- y)" 1.31 - by (rule add) (simp_all add: x y) 1.32 - also from y have "f (- y) = - f y" by (rule neg) 1.33 + also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y) 1.34 + also from _ y have "f (- y) = - f y" by (rule neg) 1.35 finally show ?thesis by simp 1.36 qed 1.37 1.38 text {* Every linear form yields @{text 0} for the @{text 0} vector. *} 1.39 1.40 -lemma (in vectorspace_linearform) linearform_zero [iff]: 1.41 - "f 0 = 0" 1.42 +lemma (in linearform) zero [iff]: 1.43 + includes vectorspace 1.44 + shows "f 0 = 0" 1.45 proof - 1.46 have "f 0 = f (0 - 0)" by simp 1.47 also have "\<dots> = f 0 - f 0" by (rule diff) simp_all