src/HOL/Limits.thy
changeset 50880 b22ecedde1c7
parent 50419 3177d0374701
child 50999 3de230ed0547
     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"