equal
deleted
inserted
replaced
1621 lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = DIM('a)" |
1621 lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = DIM('a)" |
1622 apply(subst card_image) using basis_inj by auto |
1622 apply(subst card_image) using basis_inj by auto |
1623 |
1623 |
1624 lemma in_span_basis: "(x::'a::euclidean_space) \<in> span (basis ` {..<DIM('a)})" |
1624 lemma in_span_basis: "(x::'a::euclidean_space) \<in> span (basis ` {..<DIM('a)})" |
1625 unfolding span_basis' .. |
1625 unfolding span_basis' .. |
1626 |
|
1627 lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)" |
|
1628 unfolding euclidean_component_def |
|
1629 apply(rule order_trans[OF real_inner_class.Cauchy_Schwarz_ineq2]) by auto |
|
1630 |
1626 |
1631 lemma norm_bound_component_le: "norm (x::'a::euclidean_space) \<le> e \<Longrightarrow> \<bar>x$$i\<bar> <= e" |
1627 lemma norm_bound_component_le: "norm (x::'a::euclidean_space) \<le> e \<Longrightarrow> \<bar>x$$i\<bar> <= e" |
1632 by (metis component_le_norm order_trans) |
1628 by (metis component_le_norm order_trans) |
1633 |
1629 |
1634 lemma norm_bound_component_lt: "norm (x::'a::euclidean_space) < e \<Longrightarrow> \<bar>x$$i\<bar> < e" |
1630 lemma norm_bound_component_lt: "norm (x::'a::euclidean_space) < e \<Longrightarrow> \<bar>x$$i\<bar> < e" |