522 lemma eventually_INF1: "i \<in> I \<Longrightarrow> eventually P (F i) \<Longrightarrow> eventually P (\<Sqinter>i\<in>I. F i)" |
522 lemma eventually_INF1: "i \<in> I \<Longrightarrow> eventually P (F i) \<Longrightarrow> eventually P (\<Sqinter>i\<in>I. F i)" |
523 using filter_leD[OF INF_lower] . |
523 using filter_leD[OF INF_lower] . |
524 |
524 |
525 lemma eventually_INF_finite: |
525 lemma eventually_INF_finite: |
526 assumes "finite A" |
526 assumes "finite A" |
527 shows "eventually P (INF x:A. F x) \<longleftrightarrow> |
527 shows "eventually P (\<Sqinter> x\<in>A. F x) \<longleftrightarrow> |
528 (\<exists>Q. (\<forall>x\<in>A. eventually (Q x) (F x)) \<and> (\<forall>y. (\<forall>x\<in>A. Q x y) \<longrightarrow> P y))" |
528 (\<exists>Q. (\<forall>x\<in>A. eventually (Q x) (F x)) \<and> (\<forall>y. (\<forall>x\<in>A. Q x y) \<longrightarrow> P y))" |
529 using assms |
529 using assms |
530 proof (induction arbitrary: P rule: finite_induct) |
530 proof (induction arbitrary: P rule: finite_induct) |
531 case (insert a A P) |
531 case (insert a A P) |
532 from insert.hyps have [simp]: "x \<noteq> a" if "x \<in> A" for x |
532 from insert.hyps have [simp]: "x \<noteq> a" if "x \<in> A" for x |
533 using that by auto |
533 using that by auto |
534 have "eventually P (INF x:insert a A. F x) \<longleftrightarrow> |
534 have "eventually P (\<Sqinter> x\<in>insert a A. F x) \<longleftrightarrow> |
535 (\<exists>Q R S. eventually Q (F a) \<and> (( (\<forall>x\<in>A. eventually (S x) (F x)) \<and> |
535 (\<exists>Q R S. eventually Q (F a) \<and> (( (\<forall>x\<in>A. eventually (S x) (F x)) \<and> |
536 (\<forall>y. (\<forall>x\<in>A. S x y) \<longrightarrow> R y)) \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x)))" |
536 (\<forall>y. (\<forall>x\<in>A. S x y) \<longrightarrow> R y)) \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x)))" |
537 unfolding ex_simps by (simp add: eventually_inf insert.IH) |
537 unfolding ex_simps by (simp add: eventually_inf insert.IH) |
538 also have "\<dots> \<longleftrightarrow> (\<exists>Q. (\<forall>x\<in>insert a A. eventually (Q x) (F x)) \<and> |
538 also have "\<dots> \<longleftrightarrow> (\<exists>Q. (\<forall>x\<in>insert a A. eventually (Q x) (F x)) \<and> |
539 (\<forall>y. (\<forall>x\<in>insert a A. Q x y) \<longrightarrow> P y))" |
539 (\<forall>y. (\<forall>x\<in>insert a A. Q x y) \<longrightarrow> P y))" |
913 by (simp add: filtermap_bot_iff) |
913 by (simp add: filtermap_bot_iff) |
914 |
914 |
915 subsection \<open>Increasing finite subsets\<close> |
915 subsection \<open>Increasing finite subsets\<close> |
916 |
916 |
917 definition finite_subsets_at_top where |
917 definition finite_subsets_at_top where |
918 "finite_subsets_at_top A = (INF X:{X. finite X \<and> X \<subseteq> A}. principal {Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A})" |
918 "finite_subsets_at_top A = (\<Sqinter> X\<in>{X. finite X \<and> X \<subseteq> A}. principal {Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A})" |
919 |
919 |
920 lemma eventually_finite_subsets_at_top: |
920 lemma eventually_finite_subsets_at_top: |
921 "eventually P (finite_subsets_at_top A) \<longleftrightarrow> |
921 "eventually P (finite_subsets_at_top A) \<longleftrightarrow> |
922 (\<exists>X. finite X \<and> X \<subseteq> A \<and> (\<forall>Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A \<longrightarrow> P Y))" |
922 (\<exists>X. finite X \<and> X \<subseteq> A \<and> (\<forall>Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A \<longrightarrow> P Y))" |
923 unfolding finite_subsets_at_top_def |
923 unfolding finite_subsets_at_top_def |
1343 |
1343 |
1344 lemma filterlim_INF_INF: |
1344 lemma filterlim_INF_INF: |
1345 "(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (\<Sqinter>i\<in>I. F i). f x :> (\<Sqinter>j\<in>J. G j)" |
1345 "(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (\<Sqinter>i\<in>I. F i). f x :> (\<Sqinter>j\<in>J. G j)" |
1346 unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono]) |
1346 unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono]) |
1347 |
1347 |
1348 lemma filterlim_INF': "x \<in> A \<Longrightarrow> filterlim f F (G x) \<Longrightarrow> filterlim f F (INF x:A. G x)" |
1348 lemma filterlim_INF': "x \<in> A \<Longrightarrow> filterlim f F (G x) \<Longrightarrow> filterlim f F (\<Sqinter> x\<in>A. G x)" |
1349 unfolding filterlim_def by (rule order.trans[OF filtermap_mono[OF INF_lower]]) |
1349 unfolding filterlim_def by (rule order.trans[OF filtermap_mono[OF INF_lower]]) |
1350 |
1350 |
1351 lemma filterlim_filtercomap_iff: "filterlim f (filtercomap g G) F \<longleftrightarrow> filterlim (g \<circ> f) G F" |
1351 lemma filterlim_filtercomap_iff: "filterlim f (filtercomap g G) F \<longleftrightarrow> filterlim (g \<circ> f) G F" |
1352 by (simp add: filterlim_def filtermap_le_iff_le_filtercomap filtercomap_filtercomap o_def) |
1352 by (simp add: filterlim_def filtermap_le_iff_le_filtercomap filtercomap_filtercomap o_def) |
1353 |
1353 |
1857 unfolding rel_filter.simps by atomize_elim((rule choice allI)+; auto) |
1857 unfolding rel_filter.simps by atomize_elim((rule choice allI)+; auto) |
1858 have id: "eventually P F = eventually P (id F)" "eventually Q G = eventually Q (id G)" |
1858 have id: "eventually P F = eventually P (id F)" "eventually Q G = eventually Q (id G)" |
1859 if "(F, G) \<in> SS'" for P Q F G by simp_all |
1859 if "(F, G) \<in> SS'" for P Q F G by simp_all |
1860 show "rel_filter A (Sup S) (Sup S')" |
1860 show "rel_filter A (Sup S) (Sup S')" |
1861 proof |
1861 proof |
1862 let ?Z = "SUP (F, G):SS'. Z F G" |
1862 let ?Z = "\<Squnion>(F, G)\<in>SS'. Z F G" |
1863 show *: "\<forall>\<^sub>F (x, y) in ?Z. A x y" using Z by(auto simp add: eventually_Sup) |
1863 show *: "\<forall>\<^sub>F (x, y) in ?Z. A x y" using Z by(auto simp add: eventually_Sup) |
1864 show "map_filter_on {(x, y). A x y} fst ?Z = Sup S" "map_filter_on {(x, y). A x y} snd ?Z = Sup S'" |
1864 show "map_filter_on {(x, y). A x y} fst ?Z = Sup S" "map_filter_on {(x, y). A x y} snd ?Z = Sup S'" |
1865 unfolding filter_eq_iff |
1865 unfolding filter_eq_iff |
1866 by(auto 4 4 simp add: id eventually_Sup eventually_map_filter_on *[simplified eventually_Sup] simp del: id_apply dest: Z) |
1866 by(auto 4 4 simp add: id eventually_Sup eventually_map_filter_on *[simplified eventually_Sup] simp del: id_apply dest: Z) |
1867 qed |
1867 qed |