proposition: Lemma inf_A3 r f x y: order r -> fgraph f -> sub (range f) (substrate r) -> domain f = x \times y -> (forall m, inc m y -> has_inf_graph r (partial_fun f x m)) -> ((has_inf_graph r f <-> has_inf_graph r (Lg y (fun m => inf_graph r (partial_fun f x m)))) /\ (has_inf_graph r f -> inf_graph r f = inf_graph r (Lg y (fun m => inf_graph r (partial_fun f x m))))).
proof: Proof. move=> or fgf sr df alinf. set (c:= Lg y (fun m => x \times (singleton m))). have co1: fgraph c by rewrite /c; fprops. have co2: (domain f) = (unionb c). rewrite /c df; set_extens t. move => /setX_P [pt Px Qy]. apply/setUb_P1; ex_tac; apply: setX_i; fprops. move /setUb_P1 => [z zy /setX_P [pt Px /set1_P Qy]]. apply: setX_i; fprops; ue. have dc: y = domain c by rewrite /c; aw. have pfx: forall m, inc m y -> partial_fun f x m = restr f (Vg c m). by move=> m my; rewrite LgV. have hsg: forall l, inc l (domain c) -> has_inf_graph r (restr f (Vg c l)). by move=> l; rewrite -dc=> ld; rewrite - pfx //;apply: alinf. have <-: Lg (domain c) (fun l => inf_graph r (restr f (Vg c l))) = Lg y (fun m : Set => inf_graph r (partial_fun f x m)). by rewrite -dc; apply: Lg_exten; move=> t ty /=; rewrite pfx. exact: inf_A2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)