equal
deleted
inserted
replaced
115 qed |
115 qed |
116 |
116 |
117 subclass real_normed_vector |
117 subclass real_normed_vector |
118 proof |
118 proof |
119 fix a :: real and x y :: 'a |
119 fix a :: real and x y :: 'a |
120 show "0 \<le> norm x" |
|
121 unfolding norm_eq_sqrt_inner by simp |
|
122 show "norm x = 0 \<longleftrightarrow> x = 0" |
120 show "norm x = 0 \<longleftrightarrow> x = 0" |
123 unfolding norm_eq_sqrt_inner by simp |
121 unfolding norm_eq_sqrt_inner by simp |
124 show "norm (x + y) \<le> norm x + norm y" |
122 show "norm (x + y) \<le> norm x + norm y" |
125 proof (rule power2_le_imp_le) |
123 proof (rule power2_le_imp_le) |
126 have "inner x y \<le> norm x * norm y" |
124 have "inner x y \<le> norm x * norm y" |