equal
deleted
inserted
replaced
103 lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S" |
103 lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S" |
104 unfolding from_nat_into_def[abs_def] |
104 unfolding from_nat_into_def[abs_def] |
105 using to_nat_on_infinite[of S, unfolded bij_betw_def] |
105 using to_nat_on_infinite[of S, unfolded bij_betw_def] |
106 by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite) |
106 by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite) |
107 |
107 |
|
108 lemma countable_as_injective_image: |
|
109 assumes "countable A" "infinite A" |
|
110 obtains f :: "nat \<Rightarrow> 'a" where "A = range f" "inj f" |
|
111 by (metis bij_betw_def bij_betw_from_nat_into [OF assms]) |
|
112 |
108 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A" |
113 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A" |
109 using to_nat_on_infinite[of A] to_nat_on_finite[of A] |
114 using to_nat_on_infinite[of A] to_nat_on_finite[of A] |
110 by (cases "finite A") (auto simp: bij_betw_def) |
115 by (cases "finite A") (auto simp: bij_betw_def) |
111 |
116 |
112 lemma to_nat_on_inj[simp]: |
117 lemma to_nat_on_inj[simp]: |