proposition: Theorem inf_in_product_alt g A (f := fam_of_substrates g) (Ai:= fun i => (Vfs (pr_i f i) A)) (has_inf := forall i, inc i (domain g) -> has_infimum (Vg g i) (Ai i)): order_fam g -> sub A (productb f) -> ((has_inf <-> has_infimum (order_product g) A) /\ (has_inf -> infimum (order_product g) A = Lg (domain g) (fun i => infimum (Vg g i) (Ai i)))).
proof: Proof. move=> po Ab. have fgf: fgraph f by apply: fos_graph. have df: domain f = domain g by rewrite /f; aw. have als: forall i, inc i (domain g) -> substrate (Vg g i) = Vg f i. by move=> i id; rewrite LgV. have Asi: forall i, inc i (domain g) -> sub A (source (pr_i f i)). by move=> i idg; rewrite /pr_i; aw. have afi: forall i, inc i (domain g) -> function (pr_i f i). move => i idg; apply: pri_f =>//; ue. have Ais:=(sup_in_product_aux po Ab). have p1: (has_inf -> (forall i, inc i (domain g) -> greatest_lower_bound (Vg g i) (Ai i) (infimum (Vg g i) (Ai i)))). move => hts i idg; apply: (infimum_pr1 (po _ idg)); apply: hts =>//. set mysup := Lg _ _. move:(order_product_osr po) => [opg srg]. have hlu: has_inf -> greatest_lower_bound (order_product g) A mysup. move=> hst. have mp: inc mysup (productb f). rewrite /mysup; apply/setXb_P;split => //; [fprops | by aw |]. rewrite df; move=> i idg; rewrite LgV //. by rewrite -als //; apply: inc_infimum_substrate; fprops; apply: Ais. have sas :sub A (substrate (order_product g)) by ue. apply/(glbP opg sas);split. split; first by ue. move=> y yA; apply/order_product_gleP => //. split => //;first by apply: Ab. move=> i idg; rewrite LgV //. move: (infimum_pr (po _ idg) (Ais _ idg) (hst _ idg)). move=> [[_ h]_]; apply: h. apply /(Vf_image_P (afi _ idg) (Asi _ idg)). by ex_tac; rewrite -df in idg; rewrite (pri_V idg (Ab _ yA)). move=> z [zs zp]; apply /order_product_gleP => //. split => //; first by rewrite srg in zs. move=> i idg. move: (infimum_pr (po _ idg) (Ais _ idg) (hst _ idg)). rewrite LgV//; move=> [_]; apply. split; first by apply:prod_of_substrates_p => //; move: zs; ue. move: (Asi _ idg) => As. move=> y; move /(Vf_image_P (afi _ idg) (Asi _ idg)) => [u uA ->]. rewrite -df in idg; rewrite (pri_V idg (Ab _ uA)). move: (zp _ uA) => /(order_product_gleP) [_ _]; apply; ue. have hsu: has_inf -> has_infimum (order_product g) A. by move=> hst; exists mysup; apply: hlu. have g2: has_inf-> infimum (order_product g) A = mysup. move => hst; move:(hlu hst) => s1; move:(infimum_pr1 opg (hsu hst)) => s2. by apply: (infimum_unique opg s2 s1). split=>//;split =>//. have sAs: sub A (substrate (order_product g)) by ue. move=> [x] /(glbP opg sAs) [[xs ub] lub]. move=> i idg. move: (po _ idg) => p2; move: (Ais _ idg)=> p3; move: (Asi _ idg)=> p4. have fi: function (pr_i f i) by apply: pri_f=>//; ue. exists (Vg x i); apply/(glbP p2 p3). move: xs; rewrite srg; move/(prod_of_substratesP) => [fgx dx iVs]. split. split; first by apply: iVs. move=> y /(Vf_image_P (afi _ idg) (Asi _ idg)) [u uA ->]. rewrite -df in idg; rewrite (pri_V idg (Ab _ uA)). move: (ub _ uA) => /(order_product_gleP) [_ _ ]; apply; ue. move=> z [zs h4]. set (y:= Lg (domain g) (fun j=> Yo(j = i) z (Vg x j))). have ->: (z = Vg y i) by rewrite LgV//; Ytac0. have yp: inc y (productb f). apply/setXb_P; rewrite /y df;split; aw; fprops. move=> k kd; rewrite LgV// -als//;Ytac ki; first by rewrite ki; apply: zs. by apply: iVs. have aux: (lower_bound (order_product g) A y). split;first by ue. move=> t tA; apply/(order_product_gleP); split => //; first by apply: Ab. move => k kd; rewrite LgV//. move: (ub _ tA) => /(order_product_gleP) [_ _ h5]. Ytac ki; last by apply: h5. rewrite ki; apply: h4; apply/(Vf_image_P (afi _ idg) (Asi _ idg)); ex_tac. by rewrite -df in idg; rewrite (pri_V idg (Ab _ tA)). by move: (lub _ aux) => /(order_product_gleP) [_ _ ]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)