# HG changeset patch
# User huffman
# Date 1314812551 25200
# Node ID 6820684c7a585361134c20097d698f814903b98f
# Parent  d08cb39b628a34ed08ef90f01462d2b5ddc146d3
generalize lemma isCont_vec_nth

diff -r d08cb39b628a -r 6820684c7a58 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- 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 ..