equal
deleted
inserted
replaced
203 with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net" |
203 with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net" |
204 by (rule topological_tendstoD) |
204 by (rule topological_tendstoD) |
205 then show "eventually (\<lambda>x. f x $ i \<in> S) net" |
205 then show "eventually (\<lambda>x. f x $ i \<in> S) net" |
206 by simp |
206 by simp |
207 qed |
207 qed |
|
208 |
|
209 lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a" |
|
210 unfolding isCont_def by (rule tendsto_vec_nth) |
208 |
211 |
209 lemma eventually_Ball_finite: (* TODO: move *) |
212 lemma eventually_Ball_finite: (* TODO: move *) |
210 assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net" |
213 assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net" |
211 shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net" |
214 shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net" |
212 using assms by (induct set: finite, simp, simp add: eventually_conj) |
215 using assms by (induct set: finite, simp, simp add: eventually_conj) |
433 apply (rule vector_add_component) |
436 apply (rule vector_add_component) |
434 apply (rule vector_scaleR_component) |
437 apply (rule vector_scaleR_component) |
435 apply (rule_tac x="1" in exI, simp add: norm_nth_le) |
438 apply (rule_tac x="1" in exI, simp add: norm_nth_le) |
436 done |
439 done |
437 |
440 |
438 lemmas isCont_vec_nth [simp] = |
|
439 bounded_linear.isCont [OF bounded_linear_vec_nth] |
|
440 |
|
441 instance vec :: (banach, finite) banach .. |
441 instance vec :: (banach, finite) banach .. |
442 |
442 |
443 |
443 |
444 subsection {* Inner product space *} |
444 subsection {* Inner product space *} |
445 |
445 |