proposition: Theorem inf_A2: (forall l, inc l (domain c) -> has_inf_graph r (restr f (Vg c l))) -> ((has_inf_graph r f <-> has_inf_graph r (Lg (domain c)(fun l => inf_graph r (restr f (Vg c l))))) /\ (has_inf_graph r f -> inf_graph r f = inf_graph r (Lg (domain c) (fun l => inf_graph r (restr f (Vg c l)))))).
proof: Proof. move=> alsup. split; first by apply: inf_A1=>//. move=> hyp; rewrite /inf_graph. set (g:= Lg (domain c) (fun l => inf_graph r (restr f (Vg c l)))). move: (inf_graph_pr1 or rf hyp)=> lu. rewrite -(infimum_unique or lu (infimum_pr1 or hyp)). move /(inf_A (inf_graph r f) alsup): lu => lug. have lug': greatest_lower_bound r (range g) (infimum r (range g)). by apply: infimum_pr1 => //; exists (inf_graph r f). by rewrite -(infimum_unique or lug lug'). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)