proposition: Lemma Exercise2_7f: complete_lattice r -> complete_lattice (closure_ordering).
proof: Proof. move=> [_ cl1];move: (Exercise2_7b) => [oco sco]. apply: Exercise1_11h => //; rewrite sco => X Xc. have xp1: forall f, inc f X -> closure f r. by move=> f fx; move: (Xc _ fx) => /Zo_P [ _ ]. set (iv := fun x => fun_image X (Vf ^~ x)). have ivs: (forall x, inc x (substrate r) -> sub (iv x) (substrate r)). move=> x xsr t => /funI_P [z zX ->]. move: (xp1 _ zX) => [_ s1 _]; move: (s1 _ xsr) => s2; order_tac. set (hh := fun x => infimum r (iv x)). have hp1: (forall x, inc x (substrate r) -> (lower_bound r (iv x) (hh x) /\ forall z, lower_bound r (iv x) z -> gle r z (hh x))). move=> x xsr; move:(ivs _ xsr)=> isr; move: (cl1 _ isr ) => [_ hi]. apply: (infimum_pr or isr hi). have ta: (lf_axiom hh (substrate r) (substrate r)). by move=> t tsr; move: (hp1 _ tsr) => [[ok _] _]. set (h:= Lf hh (substrate r) (substrate r)). have fh: (function h) by apply: lf_function. have p1: (forall x f, inc x (substrate r) -> inc f X -> gle r (Vf h x) (Vf f x)). move=> x f xsr fX;move: (hp1 _ xsr) => [[_ xx] _]; rewrite /h LfV//. apply: xx; apply /funI_P; ex_tac. have p2: forall x y, inc x (substrate r) -> inc y (substrate r) -> (forall f, inc f X -> gle r y (Vf f x)) -> gle r y (Vf h x). move=> x y xsr ysr h1; rewrite /h LfV//; move: (hp1 _ xsr) => [_]; apply. by split => //; move=> t /funI_P [z zX ->]; apply: h1. have p3: (increasing_fun h r r). rewrite /h;split => //; first saw; move=> x y xy. have xE: (inc x (substrate r)) by order_tac. have yE: (inc y (substrate r)) by order_tac. rewrite !LfV//; move: (hp1 _ xE)(hp1 _ yE) => [[h1 h2] _] [_]; apply. split => //; move=> z /funI_P [f fX] ->. move: (xp1 _ fX) => [[_ _ _ incf] _ _ ]. move: (incf _ _ xy) => h3. have h4: (inc (Vf f x) (iv x)) by apply /funI_P; ex_tac. move: (h2 _ h4) => h5;order_tac. have p4: (forall x, inc x (substrate r) -> gle r x (Vf h x)). move=> x xsr; apply: (p2 _ _ xsr xsr). by move=> f fX; move: (xp1 _ fX) => [_ h2 _]; apply: h2. have p5:(forall x, inc x (substrate r) -> Vf h (Vf h x) = Vf h x). move=> x xE; move: (ta _ xE) => ws. have W1: Vf h x = hh x by rewrite /h LfV. symmetry; apply: (order_antisymmetry or). by move: (p4 _ ws); rewrite -W1. move: (hp1 _ xE) => [_]; rewrite W1;apply. split; first by rewrite /h LfV//; apply: (ta _ ws). move => y /funI_P [z zX ->]. move: (p1 _ _ ws zX) => p5. move: (xp1 _ zX) => [[_ _ _ incf] _ aa]. move: (incf _ _ (p1 _ _ xE zX)); rewrite (aa _ xE) W1=> p6; order_tac. have ch: (closure h r) by split => //. 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 Wsr:sub X (substrate closure_ordering) by ue. exists h. apply /(glbP oco Wsr); split. split => //; move=> y; aw => yX;apply /Exercise2_7aP. move: (Xc _ yX)=> ys;split;fprops. move=> z [z1 z2]; apply/Exercise2_7aP; split => //; first by ue. move=> i isr; rewrite /h LfV//;move: (hp1 _ isr) => [_ ]; apply. move: z1; rewrite sco => /Zo_P [] /functionsP [fx sz tz] cz. split => //; first by rewrite -/E; Wtac; ue. move=> y /funI_P [t tX ->]. by move: (z2 _ tX) =>/Exercise2_7aP [_ _ ]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)