equal
deleted
inserted
replaced
104 by auto |
104 by auto |
105 |
105 |
106 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)" |
106 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)" |
107 unfolding fun_eq_iff by auto |
107 unfolding fun_eq_iff by auto |
108 |
108 |
109 lemmas conversep_in_rel_Id_on = |
|
110 trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]] |
|
111 |
|
112 lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)" |
109 lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)" |
113 unfolding fun_eq_iff by auto |
110 unfolding fun_eq_iff by auto |
114 |
|
115 lemmas relcompp_in_rel_Id_on = |
|
116 trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]] |
|
117 |
111 |
118 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f" |
112 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f" |
119 unfolding Gr_def Grp_def fun_eq_iff by auto |
113 unfolding Gr_def Grp_def fun_eq_iff by auto |
120 |
114 |
121 lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op =" |
115 lemma in_rel_Id_on_UNIV: "in_rel (Id_on UNIV) = op =" |