proposition: Lemma homeomorphism_cantor_like : exists f : {splitbij [set: cantor_space] >-> [set: T]}, continuous f /\ (forall A, closed A -> closed (f @` A)).
proof: Proof. exists [the {splitbij _ >-> _} of tree_map] => /=. have [cts surj inje] := projT2 (cid cantor_map); split; first exact: cts. move=> A clA; apply: (compact_closed hsdfT). apply: (@continuous_compact _ _ tree_map); first exact: continuous_subspaceT. apply: (@subclosed_compact _ _ [set: cantor_space]) => //. exact: cantor_space_compact. 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)