proposition: Lemma cantor_like_cantor_space : cantor_like cantor_space.
proof: Proof. split. - exact: cantor_perfect. - exact: cantor_space_compact. - exact: cantor_space_hausdorff. - exact: cantor_zero_dimensional. 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)