87 |
87 |
88 lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV" |
88 lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV" |
89 using countableE_infinite unfolding to_nat_on_def |
89 using countableE_infinite unfolding to_nat_on_def |
90 by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto |
90 by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto |
91 |
91 |
92 lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S" |
92 lemma bij_betw_from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S" |
93 unfolding from_nat_into_def[abs_def] |
93 unfolding from_nat_into_def[abs_def] |
94 using to_nat_on_finite[of S] |
94 using to_nat_on_finite[of S] |
95 apply (subst bij_betw_cong) |
95 apply (subst bij_betw_cong) |
96 apply (split split_if) |
96 apply (split split_if) |
97 apply (simp add: bij_betw_def) |
97 apply (simp add: bij_betw_def) |
98 apply (auto cong: bij_betw_cong |
98 apply (auto cong: bij_betw_cong |
99 intro: bij_betw_inv_into to_nat_on_finite) |
99 intro: bij_betw_inv_into to_nat_on_finite) |
100 done |
100 done |
101 |
101 |
102 lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S" |
102 lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S" |
103 unfolding from_nat_into_def[abs_def] |
103 unfolding from_nat_into_def[abs_def] |
104 using to_nat_on_infinite[of S, unfolded bij_betw_def] |
104 using to_nat_on_infinite[of S, unfolded bij_betw_def] |
105 by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite) |
105 by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite) |
106 |
106 |
107 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A" |
107 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A" |
122 unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex) |
122 unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex) |
123 |
123 |
124 lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A" |
124 lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A" |
125 using from_nat_into[of A] by auto |
125 using from_nat_into[of A] by auto |
126 |
126 |
127 lemma from_nat_into_image[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> from_nat_into A ` UNIV = A" |
127 lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = A" |
128 by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into) |
128 by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into) |
129 |
129 |
130 lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV" |
130 lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV" |
131 using to_nat_on_infinite[of A] by (simp add: bij_betw_def) |
131 using to_nat_on_infinite[of A] by (simp add: bij_betw_def) |
132 |
132 |
134 by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on) |
134 by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on) |
135 |
135 |
136 lemma to_nat_on_from_nat_into[simp]: "n \<in> to_nat_on A ` A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n" |
136 lemma to_nat_on_from_nat_into[simp]: "n \<in> to_nat_on A ` A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n" |
137 by (simp add: f_inv_into_f from_nat_into_def) |
137 by (simp add: f_inv_into_f from_nat_into_def) |
138 |
138 |
139 lemma infinite_to_nat_on_from_nat_into[simp]: |
139 lemma to_nat_on_from_nat_into_infinite[simp]: |
140 "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n" |
140 "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n" |
141 by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into) |
141 by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into) |
142 |
142 |
143 lemma from_nat_into_inj: |
143 lemma from_nat_into_inj: |
144 assumes c: "countable A" and i: "infinite A" |
144 "countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow> |
145 shows "from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" (is "?L = ?R \<longleftrightarrow> ?K") |
145 from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" |
146 proof- |
146 by (subst to_nat_on_inj[symmetric, of A]) auto |
147 have "?L = ?R \<longleftrightarrow> to_nat_on A ?L = to_nat_on A ?R" |
147 |
148 unfolding to_nat_on_inj[OF c from_nat_into[OF infinite_imp_nonempty[OF i]] |
148 lemma from_nat_into_inj_infinite[simp]: |
149 from_nat_into[OF infinite_imp_nonempty[OF i]]] .. |
149 "countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" |
150 also have "... \<longleftrightarrow> ?K" using c i by simp |
150 using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp |
151 finally show ?thesis . |
151 |
152 qed |
152 lemma eq_from_nat_into_iff: |
|
153 "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> i \<in> to_nat_on A ` A \<Longrightarrow> x = from_nat_into A i \<longleftrightarrow> i = to_nat_on A x" |
|
154 by auto |
153 |
155 |
154 lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a" |
156 lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a" |
155 by (rule exI[of _ "to_nat_on A a"]) simp |
157 by (rule exI[of _ "to_nat_on A a"]) simp |
156 |
158 |
157 lemma from_nat_into_inject[simp]: |
159 lemma from_nat_into_inject[simp]: |
158 assumes A: "A \<noteq> {}" "countable A" and B: "B \<noteq> {}" "countable B" |
160 "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B" |
159 shows "from_nat_into A = from_nat_into B \<longleftrightarrow> A = B" |
161 by (metis range_from_nat_into) |
160 by (metis assms from_nat_into_image) |
162 |
161 |
163 lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})" |
162 lemma inj_on_from_nat_into: |
164 unfolding inj_on_def by auto |
163 "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})" |
|
164 unfolding inj_on_def by auto |
|
165 |
165 |
166 subsection {* Closure properties of countability *} |
166 subsection {* Closure properties of countability *} |
167 |
167 |
168 lemma countable_SIGMA[intro, simp]: |
168 lemma countable_SIGMA[intro, simp]: |
169 "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)" |
169 "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)" |