equal
deleted
inserted
replaced
1144 |
1144 |
1145 lemma finite_set2list: |
1145 lemma finite_set2list: |
1146 assumes "finite S" |
1146 assumes "finite S" |
1147 shows "set (set2list S) = S" |
1147 shows "set (set2list S) = S" |
1148 unfolding set2list_def |
1148 unfolding set2list_def |
1149 proof (rule f_inv_f) |
1149 proof (rule f_inv_onto_f) |
1150 from `finite S` have "\<exists>l. set l = S" |
1150 from `finite S` have "\<exists>l. set l = S" |
1151 by (rule finite_list) |
1151 by (rule finite_list) |
1152 thus "S \<in> range set" |
1152 thus "S \<in> range set" |
1153 unfolding image_def |
1153 unfolding image_def |
1154 by auto |
1154 by auto |