21 by (metis sum_case_o_inj(1,2) surjective_sum) |
21 by (metis sum_case_o_inj(1,2) surjective_sum) |
22 |
22 |
23 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A" |
23 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A" |
24 by auto |
24 by auto |
25 |
25 |
26 lemma equiv_triv1: |
|
27 assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R" |
|
28 shows "(b, c) \<in> R" |
|
29 using assms unfolding equiv_def sym_def trans_def by blast |
|
30 |
|
31 lemma equiv_triv2: |
|
32 assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R" |
|
33 shows "(a, c) \<in> R" |
|
34 using assms unfolding equiv_def trans_def by blast |
|
35 |
|
36 lemma equiv_proj: |
26 lemma equiv_proj: |
37 assumes e: "equiv A R" and "z \<in> R" |
27 assumes e: "equiv A R" and "z \<in> R" |
38 shows "(proj R o fst) z = (proj R o snd) z" |
28 shows "(proj R o fst) z = (proj R o snd) z" |
39 proof - |
29 proof - |
40 from assms(2) have z: "(fst z, snd z) \<in> R" by auto |
30 from assms(2) have z: "(fst z, snd z) \<in> R" by auto |
41 have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z]) |
31 with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" |
42 have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z]) |
32 unfolding equiv_def sym_def trans_def by blast+ |
43 with P show ?thesis unfolding proj_def[abs_def] by auto |
33 then show ?thesis unfolding proj_def[abs_def] by auto |
44 qed |
34 qed |
45 |
35 |
46 (* Operators: *) |
36 (* Operators: *) |
47 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}" |
37 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}" |
48 |
38 |