equal
deleted
inserted
replaced
81 "b = (\<Sum>i\<in>Basis. f i *\<^sub>R i) \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)" |
81 "b = (\<Sum>i\<in>Basis. f i *\<^sub>R i) \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)" |
82 by (auto simp add: euclidean_representation_sum[symmetric]) |
82 by (auto simp add: euclidean_representation_sum[symmetric]) |
83 |
83 |
84 lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x" |
84 lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x" |
85 unfolding euclidean_representation_sum by simp |
85 unfolding euclidean_representation_sum by simp |
|
86 |
|
87 lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (inner x b) * (inner y b))" |
|
88 by (subst (1 2) euclidean_representation [symmetric]) |
|
89 (simp add: inner_sum_right inner_Basis ac_simps) |
86 |
90 |
87 lemma (in euclidean_space) choice_Basis_iff: |
91 lemma (in euclidean_space) choice_Basis_iff: |
88 fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool" |
92 fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool" |
89 shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))" |
93 shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))" |
90 unfolding bchoice_iff |
94 unfolding bchoice_iff |