equal
deleted
inserted
replaced
160 shows "EX f n::nat. f`A = {i. i<n} & inj_on f A" |
160 shows "EX f n::nat. f`A = {i. i<n} & inj_on f A" |
161 proof - |
161 proof - |
162 from finite_imp_nat_seg_image_inj_on[OF `finite A`] |
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" |
163 obtain f and n::nat where bij: "bij_betw f {i. i<n} A" |
164 by (auto simp:bij_betw_def) |
164 by (auto simp:bij_betw_def) |
165 let ?f = "the_inv_onto {i. i<n} f" |
165 let ?f = "the_inv_into {i. i<n} f" |
166 have "inj_on ?f A & ?f ` A = {i. i<n}" |
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]) |
167 by (fold bij_betw_def) (rule bij_betw_the_inv_into[OF bij]) |
168 thus ?thesis by blast |
168 thus ?thesis by blast |
169 qed |
169 qed |
170 |
170 |
171 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}" |
171 lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}" |
172 by(fastsimp simp: finite_conv_nat_seg_image) |
172 by(fastsimp simp: finite_conv_nat_seg_image) |