equal
deleted
inserted
replaced
1231 fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b" |
1231 fix a b assume *: "a \<in> A" "b \<in> A" and eq: "f a = f b" |
1232 show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A" |
1232 show "(f b, g a) \<in> (\<lambda>x. (f x, g x)) ` A" |
1233 using * eq[symmetric] by auto |
1233 using * eq[symmetric] by auto |
1234 qed simp_all |
1234 qed simp_all |
1235 |
1235 |
|
1236 lemma subset_fst_snd: "A \<subseteq> (fst ` A \<times> snd ` A)" |
|
1237 by force |
|
1238 |
1236 lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A" |
1239 lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A" |
1237 by(auto simp add: inj_on_def) |
1240 by(auto simp add: inj_on_def) |
1238 |
1241 |
1239 lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f" |
1242 lemma inj_apfst [simp]: "inj (apfst f) \<longleftrightarrow> inj f" |
1240 using inj_on_apfst[of f UNIV] by simp |
1243 using inj_on_apfst[of f UNIV] by simp |