# HG changeset patch
# User hoelzl
# Date 1358180219 -3600
# Node ID b22ecedde1c7e665dcd102c154b9ade9be8bf6c1
# Parent  fc394c83e490f89b6ae94a9b20ea3d32a59686d8
move eventually_Ball_finite to Limits

diff -r fc394c83e490 -r b22ecedde1c7 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon Jan 14 14:33:53 2013 +0100
+++ b/src/HOL/Limits.thy	Mon Jan 14 17:16:59 2013 +0100
@@ -68,6 +68,17 @@
   using assms unfolding eventually_def
   by (rule is_filter.conj [OF is_filter_Rep_filter])
 
+lemma eventually_Ball_finite:
+  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"
+using assms by (induct set: finite, simp, simp add: eventually_conj)
+
+lemma eventually_all_finite:
+  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
+  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
+  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
+using eventually_Ball_finite [of UNIV P] assms by simp
+
 lemma eventually_mp:
   assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   assumes "eventually (\<lambda>x. P x) F"
diff -r fc394c83e490 -r b22ecedde1c7 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Jan 14 14:33:53 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Jan 14 17:16:59 2013 +0100
@@ -210,17 +210,6 @@
 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"
-using assms by (induct set: finite, simp, simp add: eventually_conj)
-
-lemma eventually_all_finite: (* TODO: move *)
-  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
-  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
-  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
-using eventually_Ball_finite [of UNIV P] assms by simp
-
 lemma vec_tendstoI:
   assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net"
   shows "((\<lambda>x. f x) ---> a) net"