author | huffman |
Wed, 10 Aug 2011 09:23:42 -0700 | |
changeset 44133 | 691c52e900ca |
parent 44129 | 286bd57858b9 |
child 44166 | d12d89a66742 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Multivariate_Analysis/Euclidean_Space.thy |
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
2 |
Author: Johannes Hölzl, TU München |
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
3 |
Author: Brian Huffman, Portland State University |
33175 | 4 |
*) |
5 |
||
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
6 |
header {* Finite-Dimensional Inner Product Spaces *} |
33175 | 7 |
|
8 |
theory Euclidean_Space |
|
9 |
imports |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40786
diff
changeset
|
10 |
Complex_Main |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40786
diff
changeset
|
11 |
"~~/src/HOL/Library/Inner_Product" |
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
12 |
"~~/src/HOL/Library/Product_Vector" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
13 |
begin |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
14 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
15 |
subsection {* Type class of Euclidean spaces *} |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
16 |
|
44129 | 17 |
class euclidean_space = real_inner + |
18 |
fixes dimension :: "'a itself \<Rightarrow> nat" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
19 |
fixes basis :: "nat \<Rightarrow> 'a" |
44129 | 20 |
assumes DIM_positive [intro]: |
21 |
"0 < dimension TYPE('a)" |
|
22 |
assumes basis_zero [simp]: |
|
23 |
"dimension TYPE('a) \<le> i \<Longrightarrow> basis i = 0" |
|
24 |
assumes basis_orthonormal: |
|
25 |
"\<forall>i<dimension TYPE('a). \<forall>j<dimension TYPE('a). |
|
26 |
inner (basis i) (basis j) = (if i = j then 1 else 0)" |
|
27 |
assumes euclidean_all_zero: |
|
28 |
"(\<forall>i<dimension TYPE('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
29 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
30 |
syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))") |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
31 |
|
37646 | 32 |
translations "DIM('t)" == "CONST dimension (TYPE('t))" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
33 |
|
44129 | 34 |
lemma (in euclidean_space) dot_basis: |
35 |
"inner (basis i) (basis j) = (if i = j \<and> i < DIM('a) then 1 else 0)" |
|
36 |
proof (cases "(i < DIM('a) \<and> j < DIM('a))") |
|
37 |
case False |
|
38 |
hence "inner (basis i) (basis j) = 0" by auto |
|
39 |
thus ?thesis using False by auto |
|
40 |
next |
|
41 |
case True thus ?thesis using basis_orthonormal by auto |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
42 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
43 |
|
44129 | 44 |
lemma (in euclidean_space) basis_eq_0_iff [simp]: |
45 |
"basis i = 0 \<longleftrightarrow> DIM('a) \<le> i" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
46 |
proof - |
44129 | 47 |
have "inner (basis i) (basis i) = 0 \<longleftrightarrow> DIM('a) \<le> i" |
48 |
by (simp add: dot_basis) |
|
49 |
thus ?thesis by simp |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
50 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
51 |
|
44129 | 52 |
lemma (in euclidean_space) norm_basis [simp]: |
53 |
"norm (basis i) = (if i < DIM('a) then 1 else 0)" |
|
54 |
unfolding norm_eq_sqrt_inner dot_basis by simp |
|
55 |
||
56 |
lemma (in euclidean_space) basis_neq_0 [intro]: |
|
57 |
assumes "i<DIM('a)" shows "(basis i) \<noteq> 0" |
|
58 |
using assms by simp |
|
59 |
||
60 |
subsubsection {* Projecting components *} |
|
61 |
||
62 |
definition (in euclidean_space) euclidean_component (infixl "$$" 90) |
|
63 |
where "x $$ i = inner (basis i) x" |
|
64 |
||
65 |
lemma bounded_linear_euclidean_component: |
|
66 |
"bounded_linear (\<lambda>x. euclidean_component x i)" |
|
67 |
unfolding euclidean_component_def |
|
68 |
by (rule inner.bounded_linear_right) |
|
69 |
||
70 |
interpretation euclidean_component: |
|
71 |
bounded_linear "\<lambda>x. euclidean_component x i" |
|
72 |
by (rule bounded_linear_euclidean_component) |
|
73 |
||
74 |
lemma euclidean_eqI: |
|
75 |
fixes x y :: "'a::euclidean_space" |
|
76 |
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y" |
|
77 |
proof - |
|
78 |
from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0" |
|
79 |
by (simp add: euclidean_component.diff) |
|
80 |
then show "x = y" |
|
81 |
unfolding euclidean_component_def euclidean_all_zero by simp |
|
82 |
qed |
|
83 |
||
84 |
lemma euclidean_eq: |
|
85 |
fixes x y :: "'a::euclidean_space" |
|
86 |
shows "x = y \<longleftrightarrow> (\<forall>i<DIM('a). x $$ i = y $$ i)" |
|
87 |
by (auto intro: euclidean_eqI) |
|
88 |
||
89 |
lemma (in euclidean_space) basis_component [simp]: |
|
90 |
"basis i $$ j = (if i = j \<and> i < DIM('a) then 1 else 0)" |
|
91 |
unfolding euclidean_component_def dot_basis by auto |
|
92 |
||
93 |
lemma (in euclidean_space) basis_at_neq_0 [intro]: |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
94 |
"i < DIM('a) \<Longrightarrow> basis i $$ i \<noteq> 0" |
44129 | 95 |
by simp |
96 |
||
97 |
lemma (in euclidean_space) euclidean_component_ge [simp]: |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
98 |
assumes "i \<ge> DIM('a)" shows "x $$ i = 0" |
44129 | 99 |
unfolding euclidean_component_def basis_zero[OF assms] by simp |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
100 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
101 |
lemma euclidean_scaleR: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
102 |
shows "(a *\<^sub>R x) $$ i = a * (x$$i)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
103 |
unfolding euclidean_component_def by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
104 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
105 |
lemmas euclidean_simps = |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
106 |
euclidean_component.add |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
107 |
euclidean_component.diff |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
108 |
euclidean_scaleR |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
109 |
euclidean_component.minus |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
110 |
euclidean_component.setsum |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
111 |
basis_component |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
112 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
113 |
lemma euclidean_representation: |
44129 | 114 |
fixes x :: "'a::euclidean_space" |
115 |
shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)" |
|
116 |
apply (rule euclidean_eqI) |
|
117 |
apply (simp add: euclidean_component.setsum euclidean_component.scaleR) |
|
118 |
apply (simp add: if_distrib setsum_delta cong: if_cong) |
|
119 |
done |
|
120 |
||
121 |
subsubsection {* Binder notation for vectors *} |
|
122 |
||
123 |
definition (in euclidean_space) Chi (binder "\<chi>\<chi> " 10) where |
|
124 |
"(\<chi>\<chi> i. f i) = (\<Sum>i<DIM('a). f i *\<^sub>R basis i)" |
|
125 |
||
126 |
lemma euclidean_lambda_beta [simp]: |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
127 |
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)" |
44129 | 128 |
by (auto simp: euclidean_component.setsum euclidean_component.scaleR |
129 |
Chi_def if_distrib setsum_cases intro!: setsum_cong) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
130 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
131 |
lemma euclidean_lambda_beta': |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
132 |
"j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
133 |
by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
134 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
135 |
lemma euclidean_lambda_beta'':"(\<forall>j < DIM('a::euclidean_space). P j (((\<chi>\<chi> i. f i)::'a) $$ j)) \<longleftrightarrow> |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
136 |
(\<forall>j < DIM('a::euclidean_space). P j (f j))" by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
137 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
138 |
lemma euclidean_beta_reduce[simp]: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
139 |
"(\<chi>\<chi> i. x $$ i) = (x::'a::euclidean_space)" |
44129 | 140 |
by (simp add: euclidean_eq) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
141 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
142 |
lemma euclidean_lambda_beta_0[simp]: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
143 |
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ 0 = f 0" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
144 |
by (simp add: DIM_positive) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
145 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
146 |
lemma euclidean_inner: |
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
147 |
"inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))" |
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
148 |
by (subst (1 2) euclidean_representation, |
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
149 |
simp add: inner_left.setsum inner_right.setsum |
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
150 |
dot_basis if_distrib setsum_cases mult_commute) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
151 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
152 |
lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
153 |
unfolding euclidean_component_def |
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
154 |
by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp |
33175 | 155 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
156 |
subsection {* Class instances *} |
33175 | 157 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
158 |
subsubsection {* Type @{typ real} *} |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
159 |
|
44129 | 160 |
instantiation real :: euclidean_space |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
161 |
begin |
44129 | 162 |
|
163 |
definition |
|
164 |
"dimension (t::real itself) = 1" |
|
165 |
||
166 |
definition [simp]: |
|
167 |
"basis i = (if i = 0 then 1 else (0::real))" |
|
168 |
||
169 |
lemma DIM_real [simp]: "DIM(real) = 1" |
|
170 |
by (rule dimension_real_def) |
|
171 |
||
172 |
instance |
|
173 |
by default simp+ |
|
174 |
||
175 |
end |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
176 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
177 |
subsubsection {* Type @{typ complex} *} |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
178 |
|
44129 | 179 |
instantiation complex :: euclidean_space |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
180 |
begin |
44129 | 181 |
|
182 |
definition |
|
183 |
"dimension (t::complex itself) = 2" |
|
184 |
||
185 |
definition |
|
186 |
"basis i = (if i = 0 then 1 else if i = 1 then ii else 0)" |
|
187 |
||
188 |
lemma all_less_Suc: "(\<forall>i<Suc n. P i) \<longleftrightarrow> (\<forall>i<n. P i) \<and> P n" |
|
189 |
by (auto simp add: less_Suc_eq) |
|
190 |
||
191 |
instance proof |
|
192 |
show "0 < DIM(complex)" |
|
193 |
unfolding dimension_complex_def by simp |
|
194 |
next |
|
195 |
fix i :: nat |
|
196 |
assume "DIM(complex) \<le> i" thus "basis i = (0::complex)" |
|
197 |
unfolding dimension_complex_def basis_complex_def by simp |
|
198 |
next |
|
199 |
show "\<forall>i<DIM(complex). \<forall>j<DIM(complex). |
|
200 |
inner (basis i::complex) (basis j) = (if i = j then 1 else 0)" |
|
201 |
unfolding dimension_complex_def basis_complex_def inner_complex_def |
|
202 |
by (simp add: numeral_2_eq_2 all_less_Suc) |
|
203 |
next |
|
204 |
fix x :: complex |
|
205 |
show "(\<forall>i<DIM(complex). inner (basis i) x = 0) \<longleftrightarrow> x = 0" |
|
206 |
unfolding dimension_complex_def basis_complex_def inner_complex_def |
|
207 |
by (simp add: numeral_2_eq_2 all_less_Suc complex_eq_iff) |
|
208 |
qed |
|
209 |
||
210 |
end |
|
211 |
||
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
212 |
lemma DIM_complex[simp]: "DIM(complex) = 2" |
44129 | 213 |
by (rule dimension_complex_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
214 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
215 |
subsubsection {* Type @{typ "'a \<times> 'b"} *} |
38656 | 216 |
|
44129 | 217 |
instantiation prod :: (euclidean_space, euclidean_space) euclidean_space |
38656 | 218 |
begin |
219 |
||
44129 | 220 |
definition |
221 |
"dimension (t::('a \<times> 'b) itself) = DIM('a) + DIM('b)" |
|
222 |
||
223 |
definition |
|
224 |
"basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))" |
|
225 |
||
226 |
lemma all_less_sum: |
|
227 |
fixes m n :: nat |
|
228 |
shows "(\<forall>i<(m + n). P i) \<longleftrightarrow> (\<forall>i<m. P i) \<and> (\<forall>i<n. P (m + i))" |
|
229 |
by (induct n, simp, simp add: all_less_Suc) |
|
230 |
||
231 |
instance proof |
|
232 |
show "0 < DIM('a \<times> 'b)" |
|
233 |
unfolding dimension_prod_def by (intro add_pos_pos DIM_positive) |
|
234 |
next |
|
235 |
fix i :: nat |
|
236 |
assume "DIM('a \<times> 'b) \<le> i" thus "basis i = (0::'a \<times> 'b)" |
|
237 |
unfolding dimension_prod_def basis_prod_def zero_prod_def |
|
238 |
by simp |
|
239 |
next |
|
240 |
show "\<forall>i<DIM('a \<times> 'b). \<forall>j<DIM('a \<times> 'b). |
|
241 |
inner (basis i::'a \<times> 'b) (basis j) = (if i = j then 1 else 0)" |
|
242 |
unfolding dimension_prod_def basis_prod_def inner_prod_def |
|
243 |
unfolding all_less_sum prod_eq_iff |
|
244 |
by (simp add: basis_orthonormal) |
|
245 |
next |
|
246 |
fix x :: "'a \<times> 'b" |
|
247 |
show "(\<forall>i<DIM('a \<times> 'b). inner (basis i) x = 0) \<longleftrightarrow> x = 0" |
|
248 |
unfolding dimension_prod_def basis_prod_def inner_prod_def |
|
249 |
unfolding all_less_sum prod_eq_iff |
|
250 |
by (simp add: euclidean_all_zero) |
|
38656 | 251 |
qed |
44129 | 252 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
253 |
end |
38656 | 254 |
|
255 |
end |