proposition: Lemma prl_inv_hyp_prop1 S S' u: prl_same_index S S' -> prl_map2_compat S S' u -> (forall i, inc i (psI S) -> injection (Vg u i)) -> injection (projective_limit_fun S S' u).
proof: Proof. move => h1 h2 h3. move: (prl_map2_prop h1 h2) => [ [ff sf tf] _]. split =>// x y; rewrite sf => xlim ylim sv. set up := (projective_limit_fun S S' u). have hh: inc (Vf up x) (projective_limit S') by rewrite /up; Wtac. move:(prl_inv_hyp_prop h1 h2 hh);set uu := projective_limit _; move => h. have: inc y uu by rewrite -h; apply/(iim_fun_set1_P _ ff); rewrite sf. move/prl_limitP => []. move:(prl_subsets_prop (prl_inv_hyp h1 h2 hh)) => [-> _ -> ->] fgy dy yv _. move/prl_limitP: (xlim) => [fgx dx xv _]. have dxdy: domain x = domain y by move/prl_limitP: (ylim) => [_ -> _ _]. rewrite - dy -dxdy in yv. apply: fgraph_exten => // i idx. move: (h2) => [h2a h2b h2c h2d]. have idu: inc i (domain u) by rewrite h2b -dx. have iI: inc i (psI S) by rewrite -dx. move: (h2c _ iI) => [fu su tu]. have ssI:= prl_same_index_same_I h1. have iI': inc i (psI S') by rewrite - ssI. move: (yv _ idx); rewrite /prl_invim_set LgV//. move/(iim_fun_set1_P _ fu); rewrite su; move => [sa]. move: (prl_map_ax (prl_map2_prop1 h1 h2)) => ax. rewrite /up /projective_limit_fun /projective_map LfV//. rewrite /prl_map_val LgV// prl_map2_prop2 //. have xis : inc (Vg x i) (source (Vg u i)) by rewrite su; apply: xv. have yis : inc (Vg y i) (source (Vg u i)) by rewrite su. by move:(proj2 (h3 _ iI) _ _ xis yis). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)