equal
deleted
inserted
replaced
152 qed |
152 qed |
153 |
153 |
154 lemma finite_conv_nat_seg_image: |
154 lemma finite_conv_nat_seg_image: |
155 "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})" |
155 "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})" |
156 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on) |
156 by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on) |
|
157 |
|
158 lemma finite_imp_inj_to_nat_seg: |
|
159 assumes "finite A" |
|
160 shows "EX f n::nat. f`A = {i. i<n} & inj_on f A" |
|
161 proof - |
|
162 from finite_imp_nat_seg_image_inj_on[OF `finite A`] |
|
163 obtain f and n::nat where bij: "bij_betw f {i. i<n} A" |
|
164 by (auto simp:bij_betw_def) |
|
165 let ?f = "the_inv_onto {i. i<n} f" |
|
166 have "inj_on ?f A & ?f ` A = {i. i<n}" |
|
167 by (fold bij_betw_def) (rule bij_betw_the_inv_onto[OF bij]) |
|
168 thus ?thesis by blast |
|
169 qed |
157 |
170 |
158 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}" |
171 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}" |
159 by(fastsimp simp: finite_conv_nat_seg_image) |
172 by(fastsimp simp: finite_conv_nat_seg_image) |
160 |
173 |
161 |
174 |