equal
deleted
inserted
replaced
76 |
76 |
77 definition |
77 definition |
78 "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj" |
78 "(liftprj :: udom u \<rightarrow> 'a upper_pd u) = u_map\<cdot>prj" |
79 |
79 |
80 definition |
80 definition |
81 "liftdefl (t::'a upper_pd itself) = pdefl\<cdot>DEFL('a upper_pd)" |
81 "liftdefl (t::'a upper_pd itself) = liftdefl_of\<cdot>DEFL('a upper_pd)" |
82 |
82 |
83 instance proof |
83 instance proof |
84 show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)" |
84 show "ep_pair emb (prj :: udom \<rightarrow> 'a upper_pd)" |
85 unfolding emb_upper_pd_def prj_upper_pd_def |
85 unfolding emb_upper_pd_def prj_upper_pd_def |
86 by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj) |
86 by (intro ep_pair_comp ep_pair_upper ep_pair_upper_map ep_pair_emb_prj) |
109 |
109 |
110 definition |
110 definition |
111 "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj" |
111 "(liftprj :: udom u \<rightarrow> 'a lower_pd u) = u_map\<cdot>prj" |
112 |
112 |
113 definition |
113 definition |
114 "liftdefl (t::'a lower_pd itself) = pdefl\<cdot>DEFL('a lower_pd)" |
114 "liftdefl (t::'a lower_pd itself) = liftdefl_of\<cdot>DEFL('a lower_pd)" |
115 |
115 |
116 instance proof |
116 instance proof |
117 show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)" |
117 show "ep_pair emb (prj :: udom \<rightarrow> 'a lower_pd)" |
118 unfolding emb_lower_pd_def prj_lower_pd_def |
118 unfolding emb_lower_pd_def prj_lower_pd_def |
119 by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj) |
119 by (intro ep_pair_comp ep_pair_lower ep_pair_lower_map ep_pair_emb_prj) |
142 |
142 |
143 definition |
143 definition |
144 "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj" |
144 "(liftprj :: udom u \<rightarrow> 'a convex_pd u) = u_map\<cdot>prj" |
145 |
145 |
146 definition |
146 definition |
147 "liftdefl (t::'a convex_pd itself) = pdefl\<cdot>DEFL('a convex_pd)" |
147 "liftdefl (t::'a convex_pd itself) = liftdefl_of\<cdot>DEFL('a convex_pd)" |
148 |
148 |
149 instance proof |
149 instance proof |
150 show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)" |
150 show "ep_pair emb (prj :: udom \<rightarrow> 'a convex_pd)" |
151 unfolding emb_convex_pd_def prj_convex_pd_def |
151 unfolding emb_convex_pd_def prj_convex_pd_def |
152 by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj) |
152 by (intro ep_pair_comp ep_pair_convex ep_pair_convex_map ep_pair_emb_prj) |