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

src/HOL/Hahn_Banach/Normed_Space.thy

changeset 44887 | 7ca82df6e951 |

parent 31795 | be3e1cc5005c |

child 46867 | 0883804b67bb |

1.1 --- a/src/HOL/Hahn_Banach/Normed_Space.thy Sun Sep 11 21:35:35 2011 +0200 1.2 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy Sun Sep 11 22:55:26 2011 +0200 1.3 @@ -50,8 +50,7 @@ 1.4 interpret vectorspace V by fact 1.5 assume x: "x \<in> V" 1.6 then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1) 1.7 - also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" 1.8 - by (rule abs_homogenous) 1.9 + also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous) 1.10 also have "\<dots> = \<parallel>x\<parallel>" by simp 1.11 finally show ?thesis . 1.12 qed 1.13 @@ -80,13 +79,13 @@ 1.14 declare normed_vectorspace.intro [intro?] 1.15 1.16 lemma (in normed_vectorspace) gt_zero [intro?]: 1.17 - "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>" 1.18 + assumes x: "x \<in> V" and neq: "x \<noteq> 0" 1.19 + shows "0 < \<parallel>x\<parallel>" 1.20 proof - 1.21 - assume x: "x \<in> V" and neq: "x \<noteq> 0" 1.22 from x have "0 \<le> \<parallel>x\<parallel>" .. 1.23 - also have [symmetric]: "\<dots> \<noteq> 0" 1.24 + also have "0 \<noteq> \<parallel>x\<parallel>" 1.25 proof 1.26 - assume "\<parallel>x\<parallel> = 0" 1.27 + assume "0 = \<parallel>x\<parallel>" 1.28 with x have "x = 0" by simp 1.29 with neq show False by contradiction 1.30 qed