equal
deleted
inserted
replaced
902 by (perm_simp) (rule refl) |
902 by (perm_simp) (rule refl) |
903 |
903 |
904 lemma image_eqvt [eqvt]: |
904 lemma image_eqvt [eqvt]: |
905 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
905 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
906 unfolding image_def |
906 unfolding image_def |
|
907 by (perm_simp) (rule refl) |
|
908 |
|
909 lemma Image_eqvt [eqvt]: |
|
910 shows "p \<bullet> (R `` A) = (p \<bullet> R) `` (p \<bullet> A)" |
|
911 unfolding Image_def |
907 by (perm_simp) (rule refl) |
912 by (perm_simp) (rule refl) |
908 |
913 |
909 lemma UNIV_eqvt [eqvt]: |
914 lemma UNIV_eqvt [eqvt]: |
910 shows "p \<bullet> UNIV = UNIV" |
915 shows "p \<bullet> UNIV = UNIV" |
911 unfolding UNIV_def |
916 unfolding UNIV_def |