equal
deleted
inserted
replaced
198 |
198 |
199 lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z" |
199 lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z" |
200 by (simp add: the_inv_f_f) |
200 by (simp add: the_inv_f_f) |
201 |
201 |
202 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y" |
202 lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y" |
203 unfolding vimage2p_def by - |
203 unfolding vimage2p_def . |
204 |
204 |
205 lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)" |
205 lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)" |
206 unfolding rel_fun_def vimage2p_def by auto |
206 unfolding rel_fun_def vimage2p_def by auto |
207 |
207 |
208 lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (case_prod (vimage2p f g R)) \<subseteq> Collect (case_prod R)" |
208 lemma convol_image_vimage2p: "\<langle>f \<circ> fst, g \<circ> snd\<rangle> ` Collect (case_prod (vimage2p f g R)) \<subseteq> Collect (case_prod R)" |