proposition: Lemma accessible_kolmogorov : accessible_space -> kolmogorov_space.
proof: Proof. move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split=> //. by rewrite nbhsE inE; exists A => //; rewrite inE in xA. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed