equal
deleted
inserted
replaced
50 lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0" |
50 lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0" |
51 by clarsimp |
51 by clarsimp |
52 |
52 |
53 lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis" |
53 lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis" |
54 by (metis ex_in_conv nonempty_Basis someI_ex) |
54 by (metis ex_in_conv nonempty_Basis someI_ex) |
|
55 |
|
56 lemma norm_some_Basis [simp]: "norm (SOME i. i \<in> Basis) = 1" |
|
57 by (simp add: SOME_Basis) |
55 |
58 |
56 lemma (in euclidean_space) inner_sum_left_Basis[simp]: |
59 lemma (in euclidean_space) inner_sum_left_Basis[simp]: |
57 "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b" |
60 "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b" |
58 by (simp add: inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.If_cases) |
61 by (simp add: inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.If_cases) |
59 |
62 |