equal
deleted
inserted
replaced
1197 |
1197 |
1198 lemma supp_finite_set_at_base: |
1198 lemma supp_finite_set_at_base: |
1199 assumes a: "finite S" |
1199 assumes a: "finite S" |
1200 shows "supp S = atom ` S" |
1200 shows "supp S = atom ` S" |
1201 proof - |
1201 proof - |
1202 have fin: "finite (atom ` S)" |
1202 have fin: "finite (atom ` S)" using a by simp |
1203 using a by (simp add: finite_imageI) |
|
1204 have "supp S = supp (atom ` S)" by (rule atom_image_supp) |
1203 have "supp S = supp (atom ` S)" by (rule atom_image_supp) |
1205 also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set) |
1204 also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set) |
1206 finally show "supp S = atom ` S" by simp |
1205 finally show "supp S = atom ` S" by simp |
1207 qed |
1206 qed |
1208 |
1207 |