proposition: Theorem inf_in_product 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 => ofg sA. move: (order_product_opp_osr ofg). set g' := fam_of_opp g. set f' := fam_of_substrates g'. move => [[Ha Hb] Hc]. have hb: domain g = domain g' by rewrite /g' /fam_of_opp; aw. have ha: allf g sgraph by move => i /ofg []. move: (fam_of_opp_sr ha); rewrite -/f -/g' -/f' => ff'. have hc: order_fam g' by apply:fam_of_opp_or. have hd:sub A (productb f') by rewrite - ff'. have Hd: forall i, inc i (domain g) -> order (Vg g i) by []. have He:=(sup_in_product_aux ofg sA). set hi':= forall i, inc i (domain g') -> has_supremum (Vg g' i) (Vfs (pr_i f' i) A). have ra: has_inf <-> hi'. rewrite /has_inf /hi' /g' -ff' /fam_of_opp; aw; split => H i idg. have pa: order (Vg g i) by apply: Hd. have pb: has_infimum (Vg g i) (Ai i) by apply:H. rewrite LgV//. by move:(H _ idg) => [w ww]; exists w; apply /inf_sup_oppP => //; apply:He. have pa: order (Vg g i) by apply: Hd. have pb: sub (Ai i) (substrate (Vg g i)) by apply: He. move: (H _ idg) => [w ww]; exists w; apply/inf_sup_oppP => //; move: ww; aw. rewrite LgV//. have Hf: (prod_of_substrates g') = (prod_of_substrates g). by rewrite /prod_of_substrates -/f -/f' ff'. have [opg spg]:= (order_product_osr ofg). have Hg: sub A (substrate (order_product g')) by rewrite Hb. have Hg': sub A (substrate (order_product g)) by ue. have rb:has_infimum (order_product g) A <-> has_supremum (order_product g') A. split; move =>[x xinf]; exists x; rewrite ? Hc; apply/inf_sup_oppP => //; ue. move:(sup_in_product hc hd); rewrite -/hi'; move => [sa sb]. have sa': has_inf <-> has_infimum (order_product g) A. by apply:(iff_trans ra); apply: (iff_trans sa); apply: iff_sym. split => // hiT; move/sa':(hiT) => hif. move/ra:(hiT) => hiT'; move: (sb hiT'). move: (proj2(inf_sup_opp opg Hg' hif)). rewrite -Hc -hb => -> ->; apply:Lg_exten => i idg. rewrite -/f' -ff' LgV//. exact: (proj2(inf_sup_opp (Hd _ idg) (He _ idg) (hiT _ idg))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)