equal
deleted
inserted
replaced
152 by (metis mem_Collect_eq image_eqI subsetD) |
152 by (metis mem_Collect_eq image_eqI subsetD) |
153 |
153 |
154 lemma |
154 lemma |
155 "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow> |
155 "(\<lambda>x. f (f x)) ` ((\<lambda>x. Suc(f x)) ` {x. even x}) \<subseteq> A \<Longrightarrow> |
156 (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)" |
156 (\<forall>x. even x --> f (f (Suc(f x))) \<in> A)" |
157 by (metis mem_Collect_eq imageI set_rev_mp) |
157 by (metis mem_Collect_eq imageI rev_subsetD) |
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)" |