proposition: Lemma Exercise1_11g r r': order r -> order r' -> complete_lattice r' -> complete_lattice (increasing_mappings_order r r').
proof: Proof. move=> or or' clr; move: (imo_osr r or') => [ori pb]. apply: Exercise1_11b => //; rewrite pb. set (E:=substrate r); set (E':=substrate r'). move=> X Xsi. set (img:= fun x => fun_image X (fun f => Vf f x)). have se: (forall x, inc x E -> sub (img x) E'). move=> x xE t /funI_P [z zX ->]. move: (Xsi _ zX) => /soimP [[fz sz tez] iz]. rewrite /E' -tez; apply: Vf_target => //; ue. set (f:= fun x=> supremum r' (img x)). have fp1: (forall x, inc x E -> least_upper_bound r' (img x) (f x)). move=> x xE; apply: supremum_pr1 => //. exact: (proj1 ((proj2 clr) _ (se _ xE))). have ta: (lf_axiom f E E'). by move=> t tE; move: (fp1 _ tE) => /(lubP or' (se _ tE)) [[ti _] _]. have ff: (function (Lf f E E')) by apply: lf_function. have ffj:function_prop (Lf f E E') (substrate r) (substrate r') by saw. have ffi: (inc (Lf f E E') (increasing_mappings r r')). apply /soimP; split => //;saw => x y xy. move:(arg1_sr xy)(arg2_sr xy); rewrite -/E => xE yE. rewrite /f LfV // LfV //. move: (se _ xE) (se _ yE) => a1 a2. move:(fp1 _ xE)(fp1 _ yE)=> /(lubP or' a1) [_ p2] /(lubP or' a2)[[h1 h2] _]. apply: p2; split=>//; move=> t /funI_P [z zX ->]. have wi: (inc (Vf z y) (img y)) by apply /funI_P; exists z. move: (h2 _ wi) => le1. move: (Xsi _ zX) => /soimP [_ [_ _ _ df]]; move: (df _ _ xy)=> le2; order_tac. have Xs: sub X (substrate (increasing_mappings_order r r')) by rewrite pb. exists (Lf f E E'); apply /(lubP ori Xs); split. split; first by rewrite pb. move=> y yX;move: (Xsi _ yX) =>/soimP [pa incy]. apply /imo_gleP => //; split; fprops; split; fprops. move=> i isr; rewrite LfV//; move: (se _ isr)=> sei. move:(fp1 _ isr) => /(lubP or' sei) [[_ fiu] _]; apply: fiu. apply /funI_P;ex_tac. move=> z []; rewrite pb=> zs zu; apply /imo_gleP => //; split => //. move:zs => /soimP [fpy incy]; split => // i ise; rewrite LfV //. move: (se _ ise)=> sei; move: (fp1 _ ise) => /(lubP or' sei) [h1 h2]. move:(fpy) => [fy sy ty]. apply: h2; split; first Wtac. move=> y /funI_P [t tX ->]; apply: (imo_incr or' (zu _ tX) ise). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)