proposition: Lemma discrete_zero_dimension {T} : discrete_space T -> zero_dimensional T.
proof: Proof. move=> dctT x y xny; exists [set x]; split => //; last exact/nesym/eqP. by split; [exact: discrete_open | exact: discrete_closed]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed