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