proposition: Lemma Exercise1_9 I1 I2 f: fgraph f -> domain f = I1 \times I2 -> finite_set I1 -> finite_set I2 -> nonempty I1 -> nonempty I2 -> sub (range f) (substrate r) -> gle r (sup_graph r (Lg I2 (fun j => inf_graph r (Lg I1 (fun i => Vg f (J i j)))))) (inf_graph r (Lg I1 (fun i => sup_graph r (Lg I2 (fun j => Vg f (J i j)))))).
proof: Proof. move=> fgf df fs1 fs2 ni1 ni2 srf. have or: order r by move: lr => [ok _]. have hb: forall i j, inc i I1 -> inc j I2 -> inc (Vg f (J i j)) (substrate r). move=> i j i1 j2;apply: srf; apply: inc_V_range => //; rewrite df; fprops. have Hu: forall b, inc b I2 -> Hf (Lg I1 (fun i => Vg f (J i b))). by move => b bp; split; aww =>t' /Lg_range_P [b' bi1'] ->; apply: hb. have Hv: forall b, inc b I1 -> Hf (Lg I2 (fun j => Vg f (J b j))). by move => b bp; split;aww =>t' /Lg_range_P [b' bi1'] ->; apply: hb. have Ha: Hf (Lg I2 (fun j => inf_graph r (Lg I1 (fun i=> Vg f (J i j))))). split => //; aww. move=>t /Lg_range_P[b bi2] ->; apply: lattice_finite_inf5 => //; aw; fprops. have Hb: Hf (Lg I1 (fun i => sup_graph r (Lg I2 (fun j => Vg f (J i j))))). split => //; aww. move=>t/Lg_range_P [b bi2] ->; apply: lattice_finite_sup5 => //; aw; fprops. apply /lattice_finite_sup4P => //. aw; move => z zI; rewrite ! LgV//. apply/(lattice_finite_inf4P Hb); aw => t tI. rewrite LgV//. apply: (@order_transitivity _ _ (Vg f (J t z))) => //. set (fa:= (Lg I1 (fun i => Vg f (J i z)))). have Hfa: Hf fa. by rewrite /fa; split;aww => y /Lg_range_P [x xI1] ->; aw; apply: hb. have: (gle r (inf_graph r fa) (inf_graph r fa)). by order_tac; apply: lattice_finite_inf5. have ->: (Vg f (J t z) = Vg fa t). by rewrite /fa; rewrite LgV//. by move/(lattice_finite_inf4P Hfa); apply; rewrite /fa; aw. set (fb:= Lg I2 (fun j => Vg f (J t j))). have Hfa: Hf fb. by rewrite /fb; split; aww => y /Lg_range_P [x xI1] ->; apply: hb. have ->: (Vg f (J t z) = Vg fb z) by rewrite /fb LgV//. have: (gle r (sup_graph r fb) (sup_graph r fb)). by order_tac; apply: lattice_finite_sup5. by move /(lattice_finite_sup4P Hfa); apply; rewrite /fb; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)