move eventually_Ball_finite to Limits
authorhoelzl
Mon Jan 14 17:16:59 2013 +0100 (2013-01-14)
changeset 50880b22ecedde1c7
parent 50879 fc394c83e490
child 50881 ae630bab13da
move eventually_Ball_finite to Limits
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
     1.1 --- a/src/HOL/Limits.thy	Mon Jan 14 14:33:53 2013 +0100
     1.2 +++ b/src/HOL/Limits.thy	Mon Jan 14 17:16:59 2013 +0100
     1.3 @@ -68,6 +68,17 @@
     1.4    using assms unfolding eventually_def
     1.5    by (rule is_filter.conj [OF is_filter_Rep_filter])
     1.6  
     1.7 +lemma eventually_Ball_finite:
     1.8 +  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
     1.9 +  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
    1.10 +using assms by (induct set: finite, simp, simp add: eventually_conj)
    1.11 +
    1.12 +lemma eventually_all_finite:
    1.13 +  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
    1.14 +  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
    1.15 +  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
    1.16 +using eventually_Ball_finite [of UNIV P] assms by simp
    1.17 +
    1.18  lemma eventually_mp:
    1.19    assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.20    assumes "eventually (\<lambda>x. P x) F"
     2.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Jan 14 14:33:53 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Jan 14 17:16:59 2013 +0100
     2.3 @@ -210,17 +210,6 @@
     2.4  lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a"
     2.5    unfolding isCont_def by (rule tendsto_vec_nth)
     2.6  
     2.7 -lemma eventually_Ball_finite: (* TODO: move *)
     2.8 -  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
     2.9 -  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
    2.10 -using assms by (induct set: finite, simp, simp add: eventually_conj)
    2.11 -
    2.12 -lemma eventually_all_finite: (* TODO: move *)
    2.13 -  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
    2.14 -  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
    2.15 -  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
    2.16 -using eventually_Ball_finite [of UNIV P] assms by simp
    2.17 -
    2.18  lemma vec_tendstoI:
    2.19    assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net"
    2.20    shows "((\<lambda>x. f x) ---> a) net"