proposition: Lemma cantor_space_hausdorff : hausdorff_space cantor_space.
proof: Proof. apply: hausdorff_product => ?; apply: discrete_hausdorff. exact: discrete_pointed. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum interval rat) mathcomp(finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) reals signed topology HB(structures)