equal
deleted
inserted
replaced
51 "f o Abs = g ==> g o Rep = f" |
51 "f o Abs = g ==> g o Rep = f" |
52 using Rep_inverse by (auto intro: ext) |
52 using Rep_inverse by (auto intro: ext) |
53 |
53 |
54 lemma set_Rep: |
54 lemma set_Rep: |
55 "A = range Rep" |
55 "A = range Rep" |
56 proof (rule set_ext) |
56 proof (rule set_eqI) |
57 fix x |
57 fix x |
58 show "(x \<in> A) = (x \<in> range Rep)" |
58 show "(x \<in> A) = (x \<in> range Rep)" |
59 by (auto dest: Abs_inverse [of x, symmetric]) |
59 by (auto dest: Abs_inverse [of x, symmetric]) |
60 qed |
60 qed |
61 |
61 |
62 lemma set_Rep_Abs: "A = range (Rep o Abs)" |
62 lemma set_Rep_Abs: "A = range (Rep o Abs)" |
63 proof (rule set_ext) |
63 proof (rule set_eqI) |
64 fix x |
64 fix x |
65 show "(x \<in> A) = (x \<in> range (Rep o Abs))" |
65 show "(x \<in> A) = (x \<in> range (Rep o Abs))" |
66 by (auto dest: Abs_inverse [of x, symmetric]) |
66 by (auto dest: Abs_inverse [of x, symmetric]) |
67 qed |
67 qed |
68 |
68 |