src/HOL/Library/Infinite_Set.thy
changeset 34113 dbc0fb6e7eae
parent 34112 ca842111d698
child 34941 156925dd67af
     1.1 --- a/src/HOL/Library/Infinite_Set.thy	Thu Dec 17 09:33:30 2009 -0800
     1.2 +++ b/src/HOL/Library/Infinite_Set.thy	Thu Dec 17 13:49:36 2009 -0800
     1.3 @@ -433,6 +433,13 @@
     1.4    "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
     1.5    by (simp add: MOST_conj_distrib)
     1.6  
     1.7 +lemma INFM_conjI:
     1.8 +  "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
     1.9 +  unfolding MOST_iff_cofinite INFM_iff_infinite
    1.10 +  apply (drule (1) Diff_infinite_finite)
    1.11 +  apply (simp add: Collect_conj_eq Collect_neg_eq)
    1.12 +  done
    1.13 +
    1.14  lemma MOST_rev_mp:
    1.15    assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
    1.16    shows "\<forall>\<^sub>\<infinity>x. Q x"