equal
deleted
inserted
replaced
48 shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>" |
48 shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>" |
49 proof - |
49 proof - |
50 interpret vectorspace V by fact |
50 interpret vectorspace V by fact |
51 assume x: "x \<in> V" |
51 assume x: "x \<in> V" |
52 then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1) |
52 then have "- x = - 1 \<cdot> x" by (simp only: negate_eq1) |
53 also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" |
53 also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous) |
54 by (rule abs_homogenous) |
|
55 also have "\<dots> = \<parallel>x\<parallel>" by simp |
54 also have "\<dots> = \<parallel>x\<parallel>" by simp |
56 finally show ?thesis . |
55 finally show ?thesis . |
57 qed |
56 qed |
58 |
57 |
59 |
58 |
78 locale normed_vectorspace = vectorspace + norm |
77 locale normed_vectorspace = vectorspace + norm |
79 |
78 |
80 declare normed_vectorspace.intro [intro?] |
79 declare normed_vectorspace.intro [intro?] |
81 |
80 |
82 lemma (in normed_vectorspace) gt_zero [intro?]: |
81 lemma (in normed_vectorspace) gt_zero [intro?]: |
83 "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>" |
82 assumes x: "x \<in> V" and neq: "x \<noteq> 0" |
|
83 shows "0 < \<parallel>x\<parallel>" |
84 proof - |
84 proof - |
85 assume x: "x \<in> V" and neq: "x \<noteq> 0" |
|
86 from x have "0 \<le> \<parallel>x\<parallel>" .. |
85 from x have "0 \<le> \<parallel>x\<parallel>" .. |
87 also have [symmetric]: "\<dots> \<noteq> 0" |
86 also have "0 \<noteq> \<parallel>x\<parallel>" |
88 proof |
87 proof |
89 assume "\<parallel>x\<parallel> = 0" |
88 assume "0 = \<parallel>x\<parallel>" |
90 with x have "x = 0" by simp |
89 with x have "x = 0" by simp |
91 with neq show False by contradiction |
90 with neq show False by contradiction |
92 qed |
91 qed |
93 finally show ?thesis . |
92 finally show ?thesis . |
94 qed |
93 qed |