src/HOL/Library/Countable_Set.thy
changeset 57234 596a499318ab
parent 57025 e7fd64f82876
child 58881 b9556a055632
equal deleted inserted replaced
57233:8fcbfce2a2a9 57234:596a499318ab
   294     show False
   294     show False
   295       by auto
   295       by auto
   296   qed
   296   qed
   297 qed
   297 qed
   298 
   298 
       
   299 subsection {* Uncountable *}
       
   300 
       
   301 abbreviation uncountable where
       
   302   "uncountable A \<equiv> \<not> countable A"
       
   303 
       
   304 lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)"
       
   305   by (auto intro: inj_on_inv_into simp: countable_def)
       
   306      (metis all_not_in_conv inj_on_iff_surj subset_UNIV)
       
   307 
       
   308 lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
       
   309   unfolding bij_betw_def by (metis countable_image)
       
   310   
       
   311 lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
       
   312   by (metis countable_finite)
       
   313   
       
   314 lemma uncountable_minus_countable:
       
   315   "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
       
   316   using countable_Un[of B "A - B"] assms by auto
       
   317 
   299 end
   318 end