equal
deleted
inserted
replaced
66 proof - |
66 proof - |
67 assume "inj f" |
67 assume "inj f" |
68 hence "(THE x'. f x' = f x) = (THE x'. x' = x)" |
68 hence "(THE x'. f x' = f x) = (THE x'. x' = x)" |
69 by (simp only: inj_eq) |
69 by (simp only: inj_eq) |
70 also have "... = x" by (rule the_eq_trivial) |
70 also have "... = x" by (rule the_eq_trivial) |
71 finally (trans) show ?thesis by (unfold myinv_def) |
71 finally show ?thesis by (unfold myinv_def) |
72 qed |
72 qed |
73 |
73 |
74 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" |
74 lemma f_myinv_f: "inj f ==> y \<in> range f ==> f (myinv f y) = y" |
75 proof (unfold myinv_def) |
75 proof (unfold myinv_def) |
76 assume inj: "inj f" |
76 assume inj: "inj f" |