proposition: Lemma Exercise1_9_a r I1 I2 f (rf1 := fun j => Lg I1 (fun i => Vg f (J i j))) (rf2 := fun i => Lg I2 (fun j => Vg f (J i j))) (inf1 := (fun j => inf_graph r (rf1 j))) (sup1 := (fun i => sup_graph r (rf2 i))): fgraph f -> domain f = I1 \times I2 -> sub (range f) (substrate r) -> order r -> (forall j, inc j I2 -> has_infimum r (range (rf1 j))) -> (forall i, inc i I1 -> has_supremum r (range (rf2 i))) -> has_supremum r (range (Lg I2 inf1)) -> has_infimum r (range (Lg I1 sup1)) -> gle r (sup_graph r (Lg I2 inf1)) (inf_graph r (Lg I1 sup1)).
proof: Proof. move => fgf df rf or hi1 hs1 hs2 hi2. have ra j: inc j I2 ->sub (range (rf1 j)) (substrate r). move => jI2 t /Lg_range_P [i iI1 ->]; apply: rf; apply: (inc_V_range fgf). by rewrite df; apply: setXp_i. have rb i: inc i I1 ->sub (range (rf2 i)) (substrate r). move => iI1 t /Lg_range_P [j jI2 ->]; apply: rf; apply: (inc_V_range fgf). by rewrite df; apply: setXp_i. have rc j: inc j I2 -> lower_bound r (range (rf1 j)) (inf1 j). move => jI2; move: (ra j jI2) => qa. by move/(glbP or qa): (infimum_pr1 or (hi1 j jI2)); case. have rd i: inc i I1 -> upper_bound r (range (rf2 i)) (sup1 i). move => iI1; move: (rb i iI1) => qa. by move/(lubP or qa): (supremum_pr1 or (hs1 i iI1)); case. have re j: inc j I2 -> inc (inf1 j) (substrate r) by move => /rc []. have r1: sub (range (Lg I2 inf1)) (substrate r). by move => t /Lg_range_P [b bI2 ->]; apply: re. have r2: sub (range (Lg I1 sup1)) (substrate r). by move => t /Lg_range_P [b /rd /proj1 bI1 ->]. move / (lubP or r1): (supremum_pr1 or hs2) =>[[qa _] qb]. move / (glbP or r2): (infimum_pr1 or hi2) =>[[qc _] qd]. apply: qb; split; first exact. move => t /Lg_range_P [j jI2 ->]; apply: qd; split; first by apply: re. move => s /Lg_range_P [i iI1 ->]. set x := Vg f (J i j). apply: (@order_transitivity _ _ (Vg f (J i j))) => //. apply: (proj2 (rc _ jI2)); apply/Lg_range_P; ex_tac. apply: (proj2 (rd _ iI1)); apply/Lg_range_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)