proposition: Lemma Exercise2_7e f g: (forall x y, inc x E -> inc y E -> has_infimum r (doubleton x y)) -> inc f (closures) -> inc g (closures) -> has_infimum (closure_ordering) (doubleton f g).
proof: Proof. move=> hid fc gc. have Ht:sub (doubleton f g) (closures). by move=> t /set2_P; case => ->. move: (fc) (gc) => /Zo_P[p1 [q1 q2 q3]] /Zo_P [p3 [q4 q5 q6]]. have Ha: forall x, inc x E -> inc (Vf f x) E. move=> x xE; move: (q2 _ xE) => aux; rewrite /E; order_tac. have Hb: forall x, inc x E -> inc (Vf g x) E. move=> x xE; move: (q5 _ xE) => aux; rewrite /E; order_tac. set (hh:= fun z=> inf r (Vf f z) (Vf g z)). have hp: forall x, inc x E -> [/\ gle r (hh x) (Vf f x), gle r (hh x) (Vf g x) & forall z, gle r z (Vf f x) -> gle r z (Vf g x) -> gle r z (hh x)]. move => x xE; move: (Ha _ xE) (Hb _ xE) => fE gE. move: (inf_pr or fE gE (hid _ _ fE gE)) => [qa qb qc]; split => //. have h1: forall x, inc x E -> gle r x (hh x). move=> x xE; apply:(proj33 (hp _ xE)); [ by apply: q2 | by apply: q5 ]. have ep: forall x y, gle r x y -> (inc x E /\ inc y E). move=> x y xy; rewrite /E; split; order_tac. have h2: forall x y, gle r x y -> gle r (hh x) (hh y). move=> x y xy; move: (ep _ _ xy) => [xE yE]. move: q1 => [_ _ _ incf]; move: (incf _ _ xy) => r4. move: q4 => [_ _ _ incg]; move: (incg _ _ xy) => r5. move: (hp _ xE)=> [r1 r2 _]; apply: (proj33 (hp _ yE)); order_tac. set (h:= Lf hh E E). have ta: lf_axiom hh E E. by move => w xe; move: (h1 _ xe) => h3; rewrite /E;order_tac. have fh: function h by apply: lf_function. have ch: closure h r. split => //. split => //; first by rewrite /h; saw. rewrite /h; move=> x y xy; move: (ep _ _ xy) => [xE yE]. by rewrite !LfV//; apply: h2. by move=> x xE; rewrite /h LfV//; apply: h1. move=> x xE; move: (ta _ xE) => hE; rewrite /h (LfV ta xE) (LfV ta hE). move: (hp _ hE) => [r3 r4 _]. move: (hp _ xE) => [r5 r6 r9]. move: q1 => [_ _ _ incf]; move: (incf _ _ r5). move: q4 => [_ _ _ incg]; move: (incg _ _ r6). rewrite (q6 _ xE) (q3 _ xE) => r7 r8. move: (r9 _ (order_transitivity or r3 r8) (order_transitivity or r4 r7)). move: (h1 _ hE) => r10 r11; order_tac. move: (Exercise2_7b) => [oco sco]. have hco: inc h closures by apply: Zo_i => //; apply /functionsP; split => //; rewrite /h;aw. have hsco: inc h (substrate (closure_ordering)) by rewrite sco. have sd: sub (doubleton f g) (substrate closure_ordering) by ue. exists h. apply /(glbP oco sd); split. by split => //y /set2_P; case => ->; apply /Exercise2_7aP; split => // i isr;rewrite /h LfV //; move: (hp _ isr)=>[s1 s2 _]. move=> z [ze zh]. move: (zh _ (set2_1 f g)) (zh _ (set2_2 f g)). move /Exercise2_7aP => [zc _ s1] /Exercise2_7aP [_ _ s2]. apply/Exercise2_7aP;split => //. move=> i isr; move: (s1 _ isr)(s2 _ isr)(hp _ isr)=> s3 s4 [_ _ s5]. by rewrite /h LfV//; apply: s5. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)