src/HOL/Library/Countable_Set.thy
changeset 57025 e7fd64f82876
parent 54410 0a578fb7fb73
child 57234 596a499318ab
equal deleted inserted replaced
57024:c9e98c2498fd 57025:e7fd64f82876
   281 lemma countable_all:
   281 lemma countable_all:
   282   assumes S: "countable S"
   282   assumes S: "countable S"
   283   shows "(\<forall>s\<in>S. P s) \<longleftrightarrow> (\<forall>n::nat. from_nat_into S n \<in> S \<longrightarrow> P (from_nat_into S n))"
   283   shows "(\<forall>s\<in>S. P s) \<longleftrightarrow> (\<forall>n::nat. from_nat_into S n \<in> S \<longrightarrow> P (from_nat_into S n))"
   284   using S[THEN subset_range_from_nat_into] by auto
   284   using S[THEN subset_range_from_nat_into] by auto
   285 
   285 
       
   286 lemma finite_sequence_to_countable_set:
       
   287    assumes "countable X" obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X"
       
   288 proof -  show thesis
       
   289     apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
       
   290     apply (auto simp: image_iff Ball_def intro: from_nat_into split: split_if_asm)
       
   291   proof -
       
   292     fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m"
       
   293     with from_nat_into_surj[OF `countable X` `x \<in> X`]
       
   294     show False
       
   295       by auto
       
   296   qed
       
   297 qed
       
   298 
   286 end
   299 end