equal
deleted
inserted
replaced
135 lemma If_the_inv_into_f_f: |
135 lemma If_the_inv_into_f_f: |
136 "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow> |
136 "\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow> |
137 ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i" |
137 ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i" |
138 unfolding Func_def by (auto elim: the_inv_into_f_f) |
138 unfolding Func_def by (auto elim: the_inv_into_f_f) |
139 |
139 |
140 definition vimage2p where |
|
141 "vimage2p f g R = (\<lambda>x y. R (f x) (g y))" |
|
142 |
|
143 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y" |
140 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y" |
144 unfolding vimage2p_def by - |
141 unfolding vimage2p_def by - |
145 |
142 |
146 lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)" |
143 lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)" |
147 unfolding fun_rel_def vimage2p_def by auto |
144 unfolding fun_rel_def vimage2p_def by auto |