equal
deleted
inserted
replaced
150 lemma vimage_eqvt: |
150 lemma vimage_eqvt: |
151 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
151 shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)" |
152 unfolding vimage_def permute_fun_def [where f=f] |
152 unfolding vimage_def permute_fun_def [where f=f] |
153 unfolding Collect_eqvt2 mem_eqvt .. |
153 unfolding Collect_eqvt2 mem_eqvt .. |
154 |
154 |
155 lemma image_eqvt: |
|
156 shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)" |
|
157 unfolding permute_set_eq_image |
|
158 unfolding permute_fun_def [where f=f] |
|
159 by (simp add: image_image) |
|
160 |
|
161 lemma finite_permute_iff: |
155 lemma finite_permute_iff: |
162 shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" |
156 shows "finite (p \<bullet> A) \<longleftrightarrow> finite A" |
163 unfolding permute_set_eq_vimage |
157 unfolding permute_set_eq_vimage |
164 using bij_permute by (rule finite_vimage_iff) |
158 using bij_permute by (rule finite_vimage_iff) |
165 |
159 |