proposition: Lemma axinjmap : ax_inj_map T.
proof: Proof. move=> n m u d g Hu. have -> : fdistmap u d = fdist_convn d (fun i : 'I_m => fdist1 (u i)). by apply fdist_ext => i; rewrite /fdistmap fdistbindE// fdist_convnE. rewrite -axbarypart. - congr (<&>_ _ _); apply funext => j /=; symmetry; apply axidem => i. by rewrite supp_fdist1 inE => /eqP ->. - move=> x y xy. apply/setP => z. rewrite !supp_fdist1 !inE. case: eqP => //= ->. by rewrite eqtype.inj_eq //; exact: negbTE. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets) Reals mathcomp(Rstruct reals) ssrR Reals_ext realType_ext Ranalysis_ext ssr_ext ssralg_ext fdist jfdist_cond fsdist convex