--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Aug 31 10:24:29 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Aug 31 10:42:31 2011 -0700
@@ -206,6 +206,9 @@
by simp
qed
+lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
+ unfolding isCont_def by (rule tendsto_vec_nth)
+
lemma eventually_Ball_finite: (* TODO: move *)
assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
@@ -435,9 +438,6 @@
apply (rule_tac x="1" in exI, simp add: norm_nth_le)
done
-lemmas isCont_vec_nth [simp] =
- bounded_linear.isCont [OF bounded_linear_vec_nth]
-
instance vec :: (banach, finite) banach ..