proposition: Lemma join_product_inj : accessible_space T -> set_inj [set: T] join_product.
proof: Proof. move=> /accessible_closed_set1 cl1 x y; case: (eqVneq x y) => // xny _ _ jxjy. have [] := (@sepf [set y] x (cl1 y)); first by exact/eqP. move=> i P; suff : join_product x i != join_product y i by rewrite jxjy => /eqP. apply/negP; move: P; apply: contra_not => /eqP; rewrite /join_product => ->. by apply: subset_closure; exists y. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed