equal
deleted
inserted
replaced
158 |
158 |
159 lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)" |
159 lemma "f \<in> (\<lambda>u v. b \<times> u \<times> v) ` A \<Longrightarrow> \<forall>u v. P (b \<times> u \<times> v) \<Longrightarrow> P(f y)" |
160 by (metis (lifting) imageE) |
160 by (metis (lifting) imageE) |
161 |
161 |
162 lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)" |
162 lemma image_TimesA: "(\<lambda>(x, y). (f x, g y)) ` (A \<times> B) = (f ` A) \<times> (g ` B)" |
163 by (metis map_pair_def map_pair_surj_on) |
163 by (metis map_prod_def map_prod_surj_on) |
164 |
164 |
165 lemma image_TimesB: |
165 lemma image_TimesB: |
166 "(\<lambda>(x, y, z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f ` A) \<times> (g ` B) \<times> (h ` C)" |
166 "(\<lambda>(x, y, z). (f x, g y, h z)) ` (A \<times> B \<times> C) = (f ` A) \<times> (g ` B) \<times> (h ` C)" |
167 by force |
167 by force |
168 |
168 |