equal
deleted
inserted
replaced
147 lemma euclidean_eqI: |
147 lemma euclidean_eqI: |
148 fixes x y :: "'a::euclidean_space" |
148 fixes x y :: "'a::euclidean_space" |
149 assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y" |
149 assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y" |
150 proof - |
150 proof - |
151 from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0" |
151 from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0" |
152 by (simp add: euclidean_component_diff) |
152 by simp |
153 then show "x = y" |
153 then show "x = y" |
154 unfolding euclidean_component_def euclidean_all_zero by simp |
154 unfolding euclidean_component_def euclidean_all_zero by simp |
155 qed |
155 qed |
156 |
156 |
157 lemma euclidean_eq: |
157 lemma euclidean_eq: |