65 assumes P: "eventually (\<lambda>x. P x) F" |
65 assumes P: "eventually (\<lambda>x. P x) F" |
66 assumes Q: "eventually (\<lambda>x. Q x) F" |
66 assumes Q: "eventually (\<lambda>x. Q x) F" |
67 shows "eventually (\<lambda>x. P x \<and> Q x) F" |
67 shows "eventually (\<lambda>x. P x \<and> Q x) F" |
68 using assms unfolding eventually_def |
68 using assms unfolding eventually_def |
69 by (rule is_filter.conj [OF is_filter_Rep_filter]) |
69 by (rule is_filter.conj [OF is_filter_Rep_filter]) |
|
70 |
|
71 lemma eventually_Ball_finite: |
|
72 assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net" |
|
73 shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net" |
|
74 using assms by (induct set: finite, simp, simp add: eventually_conj) |
|
75 |
|
76 lemma eventually_all_finite: |
|
77 fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool" |
|
78 assumes "\<And>y. eventually (\<lambda>x. P x y) net" |
|
79 shows "eventually (\<lambda>x. \<forall>y. P x y) net" |
|
80 using eventually_Ball_finite [of UNIV P] assms by simp |
70 |
81 |
71 lemma eventually_mp: |
82 lemma eventually_mp: |
72 assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" |
83 assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" |
73 assumes "eventually (\<lambda>x. P x) F" |
84 assumes "eventually (\<lambda>x. P x) F" |
74 shows "eventually (\<lambda>x. Q x) F" |
85 shows "eventually (\<lambda>x. Q x) F" |