equal
deleted
inserted
replaced
745 |
745 |
746 lemma map_fset_image [simp]: |
746 lemma map_fset_image [simp]: |
747 shows "fset (map_fset f S) = f ` (fset S)" |
747 shows "fset (map_fset f S) = f ` (fset S)" |
748 by (descending) (simp) |
748 by (descending) (simp) |
749 |
749 |
750 lemma nj_map_fset_cong: |
750 lemma inj_map_fset_cong: |
751 shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T" |
751 shows "inj f \<Longrightarrow> map_fset f S = map_fset f T \<longleftrightarrow> S = T" |
752 by (descending) (metis inj_vimage_image_eq list_eq.simps set_map) |
752 by (descending) (metis inj_vimage_image_eq list_eq.simps set_map) |
753 |
753 |
754 lemma map_union_fset: |
754 lemma map_union_fset: |
755 shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T" |
755 shows "map_fset f (S |\<union>| T) = map_fset f S |\<union>| map_fset f T" |