proposition: Lemma exercise5_1 I x y: (forall i, inc i I -> sub (y i) (x i)) -> nonempty I -> productf I y = intersectionf I (fun i=> Vfi (pr_i (Lg I x) i) (y i)).
proof: Proof. move=> syxi neI. have fgL: fgraph (Lg I x) by fprops. have fpj: forall j, inc j I-> function (pr_i (Lg I x) j). by move=> j jI; apply: pri_f=>//;aw. set_extens t. move /setXf_P=> [fgt dt iVy]; apply: setIf_i=>//. move=> j jI; apply /iim_graph_P. exists (Vg t j); first by apply: iVy. have jd: inc j (domain (Lg I x)) by aw. have tp:(inc t (productb (Lg I x))). apply/setXb_P; saw => i iI. by rewrite LgV//; apply: syxi=>//; apply: iVy. by rewrite -(pri_V jd tp); Wtac; rewrite /pr_i lf_source. have rI: inc (rep I) I by apply: rep_i. move => h; move:(setIf_hi h rI) => /iim_graph_P [u uy Jg]. move: (p1graph_source (fpj _ rI) Jg). rewrite /pr_i;aw; move /setXf_P=>[fgt dt iVV]. apply/setXf_P;split => // i idt. move: (setIf_hi h idt) => /iim_graph_P [v vi Jgv]. move: (Vf_pr (fpj _ idt) Jgv); rewrite pri_V =>//; aw; trivial. by move=> <-. by apply/setXb_P; saw => k ki; rewrite LgV//; apply: iVV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)