proposition: Lemma Exercise1_9_b I1 I2 r f: fgraph f -> domain f = I1 \times I2 -> sub (range f) (substrate r) -> complete_lattice 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 => ha hb hc [or hd]. have H i j: inc i I1 -> inc j I2 -> inc (Vg f (J i j)) (substrate r). move => qa qb; apply: hc; apply: (inc_V_range ha). by rewrite hb; apply: setXp_i. have qa X: sub X (substrate r) -> has_supremum r X by case /hd. have qb X: sub X (substrate r) -> has_infimum r X by case /hd. pose R1 j := (range (Lg I1 (fun i => Vg f (J i j)))). pose R2 i := (range (Lg I2 (fun j => Vg f (J i j)))). have R1a j: inc j I2 -> sub (R1 j) (substrate r). by move => jI2 t /Lg_range_P [i iI1 ->]; apply: H. have R2a i: inc i I1 -> sub (R2 i) (substrate r). by move => iI2 t /Lg_range_P [j jI1 ->]; apply: H. have ra j: inc j I2 -> has_infimum r ( R1 j). by move => ji2; apply: qb; apply: R1a. have rb i: inc i I1 -> has_supremum r (R2 i). by move => iI1; apply: qa; apply: R2a. apply: Exercise1_9_a => //. - apply: qa =>y /Lg_range_P [j jI2 ->]. by move/(glbP or (R1a _ jI2)):(infimum_pr1 or (ra j jI2)) => [[ok _] _]. - apply: qb =>y /Lg_range_P [i iI1 ->]. by move/(lubP or (R2a _ iI1)):(supremum_pr1 or (rb i iI1)) => [[ok _] _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)