equal
deleted
inserted
replaced
1133 have "snd x = snd y" by (auto dest:dest:inj_onD) |
1133 have "snd x = snd y" by (auto dest:dest:inj_onD) |
1134 ultimately show "x = y" by(rule prod_eqI) |
1134 ultimately show "x = y" by(rule prod_eqI) |
1135 qed |
1135 qed |
1136 |
1136 |
1137 lemma map_pair_surj: |
1137 lemma map_pair_surj: |
|
1138 fixes f :: "'a \<Rightarrow> 'b" and g :: "'c \<Rightarrow> 'd" |
1138 assumes "surj f" and "surj g" |
1139 assumes "surj f" and "surj g" |
1139 shows "surj (map_pair f g)" |
1140 shows "surj (map_pair f g)" |
1140 unfolding surj_def |
1141 unfolding surj_def |
1141 proof |
1142 proof |
1142 fix y :: "'b \<times> 'd" |
1143 fix y :: "'b \<times> 'd" |