| changeset 63007 | aa894a49f77d |
| parent 62913 | 13252110a6fe |
| child 63237 | 3e908f762817 |
--- a/src/HOL/Product_Type.thy Sun Apr 17 22:38:50 2016 +0200 +++ b/src/HOL/Product_Type.thy Mon Apr 18 14:30:32 2016 +0100 @@ -1233,6 +1233,9 @@ using * eq[symmetric] by auto qed simp_all +lemma subset_fst_snd: "A \<subseteq> (fst ` A \<times> snd ` A)" + by force + lemma inj_on_apfst [simp]: "inj_on (apfst f) (A \<times> UNIV) \<longleftrightarrow> inj_on f A" by(auto simp add: inj_on_def)