diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 971b02c98f..f61c48a814 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,6 +4,23 @@
 
 ### Added
 
+- in file `cantor.v`,
+  + new definitions `cantor_space`, `cantor_like`, `pointed_discrete`, and 
+    `tree_of`.
+  + new lemmas `cantor_space_compact`, `cantor_space_hausdorff`, 
+    `cantor_zero_dimensional`, `cantor_perfect`, `cantor_like_cantor_space`, 
+    `tree_map_props`, `homeomorphism_cantor_like`, and 
+    `cantor_like_finite_prod`.
+  + new theorem `cantor_surj`.
+- in file `topology.v`,
+  + new lemmas `perfect_set2`, and `ent_closure`.
+  + lemma `clopen_surj`
+
+- in `cantor.v`:
+  + definition `pointed_discrete0`
+  + lemmas `discrete_space_pointed`, `discrete_pointed`
+  + lemma `bool_compact'`
+
 ### Changed
   
 ### Renamed
diff --git a/_CoqProject b/_CoqProject
index fb6175469e..fcb3ccc198 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -22,6 +22,7 @@ theories/reals.v
 theories/landau.v
 theories/Rstruct.v
 theories/topology.v
+theories/cantor.v
 theories/prodnormedzmodule.v
 theories/normedtype.v
 theories/realfun.v
diff --git a/theories/cantor.v b/theories/cantor.v
new file mode 100644
index 0000000000..e8466149df
--- /dev/null
+++ b/theories/cantor.v
@@ -0,0 +1,578 @@
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum.
+From mathcomp Require Import interval rat fintype finmap.
+Require Import mathcomp_extra boolp classical_sets signed functions cardinality.
+Require Import reals topology.
+From HB Require Import structures.
+
+(******************************************************************************)
+(*                      The Cantor Space and Applications                     *)
+(*                                                                            *)
+(* This file develops the theory of the Cantor space, that is bool^nat with   *)
+(* the product topology. The two main theorems proved here are                *)
+(* homeomorphism_cantor_like, and cantor_surj, a.k.a. Alexandroff-Hausdorff.  *)
+(*                                                                            *)
+(*          cantor_space == the Cantor space, with its canonical metric       *)
+(*         cantor_like T == perfect + compact + hausdroff + zero dimensional  *)
+(*    pointed_discrete T == equips T with the discrete topology               *)
+(*             tree_of T == builds a topological tree with levels (T n)       *)
+(*                                                                            *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import Order.TTheory GRing.Theory Num.Def Num.Theory.
+Import numFieldTopology.Exports.
+
+Local Open Scope classical_set_scope.
+
+Definition pointed_discrete0 (P : pointedType) : Type := P.
+HB.instance Definition _ (P : pointedType) := Pointed.on (pointed_discrete0 P).
+HB.instance Definition _ (P : pointedType) :=
+  hasNbhs.Build (pointed_discrete0 P) principal_filter.
+Lemma discrete_space_pointed (P : pointedType) :
+  discrete_space (pointed_discrete0 P).
+Proof. by []. Qed.
+Definition pointed_discrete (P : pointedType) :=
+  discrete_topology (discrete_space_pointed P).
+HB.instance Definition _ (P : pointedType) := Uniform.on (pointed_discrete P).
+HB.instance Definition _ {R} (P : pointedType) : PseudoMetric R _ :=
+  PseudoMetric.on (pointed_discrete P).
+
+Lemma discrete_pointed (T : topologicalType) :
+  discrete_space (pointed_discrete T).
+Proof.
+apply/funext => /= x; apply/funext => A; apply/propext; split.
+- by move=> [E hE EA] x0 ->{x0}; apply: EA => /=; apply: hE => /=; exists x.
+- move=> h; exists [set x | x.1 = x.2]; first by move=> -[a b] [t _] [<- <-].
+  by move=> y /= xy; exact: h.
+Qed.
+
+Definition cantor_space :=
+  prod_topology (fun _ : nat => discrete_topology discrete_bool).
+
+HB.instance Definition _ := Pointed.on cantor_space.
+HB.instance Definition _ := Nbhs.on cantor_space.
+HB.instance Definition _ := Topological.on cantor_space.
+HB.instance Definition _ := Uniform.on cantor_space.
+
+Definition cantor_like (T : topologicalType) :=
+  [/\ perfect_set [set: T],
+      compact [set: T],
+      hausdorff_space T &
+      zero_dimensional T].
+
+(* NB: bool_compact : compact [set: bool] *)
+Lemma bool_compact' : compact [set: discrete_topology discrete_bool].
+Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed.
+
+Lemma cantor_space_compact : compact [set: cantor_space].
+Proof.
+have := @tychonoff _ (fun _ : nat => _) _ (fun=> bool_compact').
+by congr (compact _); rewrite eqEsubset.
+Qed.
+
+Lemma cantor_space_hausdorff : hausdorff_space cantor_space.
+Proof.
+apply: hausdorff_product => ?; apply: discrete_hausdorff.
+exact: discrete_pointed.
+Qed.
+
+Lemma cantor_zero_dimensional : zero_dimensional cantor_space.
+Proof.
+apply: zero_dimension_prod => _; apply: discrete_zero_dimension.
+exact: discrete_pointed.
+Qed.
+
+Lemma cantor_perfect : perfect_set [set: cantor_space].
+Proof. by apply: perfect_diagonal => _; exists (true, false). Qed.
+
+Lemma cantor_like_cantor_space : cantor_like cantor_space.
+Proof.
+split.
+- exact: cantor_perfect.
+- exact: cantor_space_compact.
+- exact: cantor_space_hausdorff.
+- exact: cantor_zero_dimensional.
+Qed.
+
+(* The overall goal of the next few sections is to prove that
+        Every compact metric space `T` is the image of the Cantor space.
+   The overall proof will build two continuous functions
+             Cantor space -> a bespoke tree for `T` -> `T`
+   The proof is in 4 parts.
+
+   Part 1: Some generic machinery about continuous functions from trees.
+   Part 2: All cantor-like spaces are homeomorphic to the Cantor space.
+          (an application of part 1)
+   Part 3: Finitely branching trees are Cantor-like.
+   Part 4: Every compact metric space has a finitely branching tree with
+           a continuous surjection. (a second application of part 1)
+
+   Part 1:
+   A tree here has countable levels, and nodes of type `K n` on the nth level.
+   Each level is in the 'discrete' topology, so the nodes are independent.
+   The goal is to build a map from branches to X.
+   1. Each level of the tree corresponds to an approximation of `X`.
+   2. Each level refines the previous approximation.
+   3. Then each branch has a corresponding Cauchy filter.
+   4. The overall function from branches to X is a continuous surjection.
+   5. With an extra disjointness condition, this is also an injection
+*)
+Section topological_trees.
+Context {K : nat -> topologicalType} {X : topologicalType}
+        (refine_apx : forall n, set X -> K n -> set X)
+        (tree_invariant : set X -> Prop).
+
+Hypothesis cmptX : compact [set: X].
+Hypothesis hsdfX : hausdorff_space X.
+Hypothesis discreteK : forall n, discrete_space (K n).
+Hypothesis refine_cover : forall n U, U = \bigcup_e @refine_apx n U e.
+Hypothesis refine_invar : forall n U e,
+  tree_invariant U -> tree_invariant (@refine_apx n U e).
+Hypothesis invar_n0 : forall U, tree_invariant U -> U !=set0.
+Hypothesis invarT : tree_invariant [set: X].
+Hypothesis invar_cl : tree_invariant `<=` closed.
+Hypothesis refine_separates: forall x y : X, x != y ->
+  exists n, forall (U : set X) e,
+    @refine_apx n U e x -> ~@refine_apx n U e y.
+
+Let refine_subset n U e : @refine_apx n U e `<=` U.
+Proof. by rewrite [X in _ `<=` X](refine_cover n); exact: bigcup_sup. Qed.
+
+Let T := prod_topology K.
+
+Local Fixpoint branch_apx (b : T) n :=
+  if n is m.+1 then refine_apx (branch_apx b m) (b m) else [set: X].
+
+Let tree_mapF b := filter_from [set: nat] (branch_apx b).
+
+Let tree_map_invar b n : tree_invariant (branch_apx b n).
+Proof. by elim: n => // n ?; exact: refine_invar. Qed.
+
+Let tree_map_sub b i j : (i <= j)%N -> branch_apx b j `<=` branch_apx b i.
+Proof.
+elim: j i => [?|j IH i]; first by rewrite leqn0 => /eqP ->.
+rewrite leq_eqVlt => /predU1P[->//|/IH].
+by apply: subset_trans; exact: refine_subset.
+Qed.
+
+Instance tree_map_filter b : ProperFilter (tree_mapF b).
+Proof.
+split; first by case => n _ P; case: (invar_n0 (tree_map_invar b n)) => x /P.
+apply: filter_from_filter; first by exists 0%N.
+move=> i j _ _; exists (maxn i j)  => //; rewrite subsetI.
+by split; apply: tree_map_sub; [exact: leq_maxl | exact: leq_maxr].
+Qed.
+
+Let tree_map b := lim (tree_mapF b).
+
+Let cvg_tree_map b : cvg (tree_mapF b).
+Proof.
+have [|x [_ clx]] := cmptX (tree_map_filter b); first exact: filterT.
+apply/cvg_ex; exists x => /=; apply: (compact_cluster_set1 _ cmptX) => //.
+- exact: filterT.
+- exact: filterT.
+rewrite eqEsubset; split=> [y cly|? -> //].
+have [->//|/refine_separates[n sep]] := eqVneq x y.
+have bry : branch_apx b n.+1 y.
+  have /closure_id -> := invar_cl (tree_map_invar b n.+1).
+  by move: cly; rewrite clusterE; apply; exists n.+1.
+suff /sep : branch_apx b n.+1 x by [].
+have /closure_id -> := invar_cl (tree_map_invar b n.+1).
+by move: clx; rewrite clusterE; apply; exists n.+1.
+Qed.
+
+Local Lemma tree_map_surj : set_surj [set: T] [set: X] tree_map.
+Proof.
+move=> z _; suff : exists g, forall n, branch_apx g n z.
+  case=> g gnz; exists g => //; apply: close_eq => // U [oU Uz] V ngV; exists z.
+  by split => //; have [n _] := @cvg_tree_map g _ ngV; exact.
+have zcov' : forall n (U : set X), exists e, U z -> @refine_apx n U e z.
+  move=> n U; have [|?] := pselect (U z); last by exists point.
+  by rewrite [X in X z -> _](@refine_cover n U); case => e _ ?; exists e.
+pose zcov n U := projT1 (cid (zcov' n U)).
+pose fix g n : K n * set X :=
+  if n is m.+1
+  then (zcov m.+1 (g m).2, @refine_apx m.+1 (g m).2 (zcov m.+1 (g m).2))
+  else (zcov O [set: X], @refine_apx O [set: X] (zcov O [set: X])).
+pose g' n := (g n).1; have apxg n : branch_apx g' n.+1 = (g n).2.
+  by elim: n => //= n ->.
+exists g'; elim => // n /= IH.
+have /(_ IH) := projT2 (cid (zcov' n (branch_apx g' n))).
+by case: n {IH} => // n; rewrite apxg.
+Qed.
+
+Let tree_prefix (b : T) (n : nat) :
+  \forall c \near b, forall i,  (i < n)%N -> b i = c i.
+Proof.
+elim: n => [|n IH]; first by near=> z => ?; rewrite ltn0.
+near=> z => i; rewrite leq_eqVlt => /predU1P[|iSn]; last by rewrite (near IH z).
+move=> [->]; near: z; exists (proj n @^-1` [set b n]).
+split => //; suff : @open T (proj n @^-1` [set b n]) by [].
+by apply: open_comp; [move=> + _; exact: proj_continuous| exact: discrete_open].
+Unshelve. all: end_near. Qed.
+
+Let apx_prefix b c n :
+  (forall i, (i < n)%N -> b i = c i) -> branch_apx b n = branch_apx c n.
+Proof.
+elim: n => //= n IH inS; rewrite IH; first by rewrite inS.
+by move=> ? ?; exact/inS/ltnW.
+Qed.
+
+Let tree_map_apx b n : branch_apx b n (tree_map b).
+Proof.
+apply: (@closed_cvg _ _ _ (tree_map_filter b)); last exact: cvg_tree_map.
+  by apply: invar_cl; exact: tree_map_invar.
+by exists n.
+Qed.
+
+Local Lemma tree_map_cts : continuous tree_map.
+Proof.
+move=> b U /cvg_tree_map [n _] /filterS; apply.
+  exact/fmap_filter/nbhs_filter.
+rewrite nbhs_simpl /=; near_simpl; have := tree_prefix b n; apply: filter_app.
+by near=> z => /apx_prefix ->; exact: tree_map_apx.
+Unshelve. all: end_near. Qed.
+
+Let tree_map_setI x y n : tree_map x = tree_map y ->
+  refine_apx (branch_apx x n) (x n) `&` refine_apx (branch_apx y n) (y n) !=set0.
+Proof.
+move=> xyE; exists (tree_map y); split.
+  by rewrite -xyE -/(branch_apx x n.+1); exact: tree_map_apx.
+by rewrite -/(branch_apx y n.+1); exact: tree_map_apx.
+Qed.
+
+Local Lemma tree_map_inj : (forall n U, trivIset [set: K n] (@refine_apx n U)) ->
+  set_inj [set: T] tree_map.
+Proof.
+move=> triv x y _ _ xyE; apply: functional_extensionality_dep => n.
+suff : forall n, branch_apx x n = branch_apx y n.
+  move=> brE; apply: (@triv n (branch_apx x n) _ _ I I).
+  by rewrite [in X in _ `&` X]brE; exact: tree_map_setI.
+elim => // m /= brE.
+rewrite (@triv m (branch_apx x m) (x m) (y m) I I) 1?brE//.
+by rewrite -[in X in X `&` _]brE; exact: tree_map_setI.
+Qed.
+
+Lemma tree_map_props : exists f : T -> X,
+  [/\ continuous f,
+      set_surj [set: T] [set: X] f &
+      (forall n U, trivIset [set: K n] (@refine_apx n U)) ->
+        set_inj [set: T] f].
+Proof.
+exists tree_map; split.
+- exact: tree_map_cts.
+- exact: tree_map_surj.
+- exact: tree_map_inj.
+Qed.
+
+End topological_trees.
+
+(*
+  Part 2: We can use `tree_map_props` to build a homeomorphism from the
+  cantor_space to a Cantor-like space T.
+*)
+
+Section TreeStructure.
+Context {R : realType} {T : pseudoMetricType R}.
+Hypothesis cantorT : cantor_like T.
+
+Let dsctT : zero_dimensional T.   Proof. by case: cantorT. Qed.
+Let pftT  : perfect_set [set: T]. Proof. by case: cantorT. Qed.
+Let cmptT : compact [set: T].     Proof. by case: cantorT. Qed.
+Let hsdfT : @hausdorff_space T.   Proof. by case: cantorT. Qed.
+
+Let c_invar (U : set T) := clopen U /\ U !=set0.
+
+Let U_ := unsquash (clopen_surj cmptT).
+
+Let split_clopen' (U : set T) : exists V,
+  open U -> U !=set0 -> [/\ clopen V, V `&` U !=set0 & ~`V `&` U !=set0].
+Proof.
+have [oU|?] := pselect (open U); last by exists point.
+have [Un0|?] := pselect (U !=set0); last by exists point.
+have [x [y] [Ux] Uy xny] := (iffLR perfect_set2) pftT U oU Un0.
+have [V [clV Vx Vy]] := dsctT xny; exists V => _ _.
+by split => //; [exists x | exists y].
+Qed.
+
+Let split_clopen (U : set T) := projT1 (cid (split_clopen' U)).
+
+Let c_ind n (V : set T) (b : bool) :=
+  let Wn :=
+    if pselect ((U_ n) `&` V !=set0 /\ ~` (U_ n) `&` V !=set0)
+    then U_ n else split_clopen V in
+  (if b then Wn else ~` Wn) `&` V.
+
+Local Lemma cantor_map : exists f : cantor_space -> T,
+  [/\ continuous f,
+      set_surj [set: cantor_space] [set: T] f &
+      set_inj [set: cantor_space] f ].
+Proof.
+have [] := @tree_map_props
+    (fun=> discrete_topology discrete_bool) T c_ind c_invar cmptT hsdfT.
+- by move=> ?; exact: discrete_pointed.
+- move=> n V; rewrite eqEsubset; split => [t Vt|t [? ? []]//].
+  have [?|?] := pselect (U_ n `&` V !=set0 /\ ~` U_ n `&` V !=set0).
+  + have [Unt|Unt] := pselect (U_ n t).
+    * by exists true => //; rewrite /c_ind; case: pselect.
+    * by exists false => //; rewrite /c_ind; case: pselect.
+  + have [scVt|scVt] := pselect (split_clopen V t).
+    * by exists true => //; rewrite /c_ind; case: pselect.
+    * by exists false => //; rewrite /c_ind; case: pselect.
+- move=> n U e [] clU Un0; rewrite /c_ind; case: pselect => /=.
+  + move=> [UU CUU]; case: e => //; split => //; apply: clopenI => //.
+      exact: funS.
+    by apply: clopenC => //; exact: funS.
+  + move=> _; have [|//|clscU scUU CscUU] := projT2 (cid (split_clopen' U)).
+      by case: clU.
+    case: e; split => //; first exact: clopenI.
+    by apply: clopenI => //; exact: clopenC.
+- by move=> ? [].
+- by split; [exact: clopenT | exists point].
+- by move=> ? [[]].
+- move=> x y /dsctT [A [clA Ax Any]].
+  have [n _ UnA] := @surj _ _ _ _ U_ _ clA; exists n => V e.
+  have [|+ _] := pselect (V y); last by apply: subsetC => ? [].
+  have [Vx Vy|? _ []//] := pselect (V x).
+  rewrite {1 2}/c_ind; case: pselect => /=; rewrite ?UnA.
+    by move=> _; case: e; case => // ? ?; apply/not_andP; left.
+  by apply: absurd; split; [exists x | exists y].
+- move=> f [ctsf surjf injf]; exists f; split => //.
+  apply: injf.
+  by move=> n U i j _ _ [z] [] [] + Uz [+ _]; move: i j => [] [].
+Qed.
+
+Let tree_map := projT1 (cid cantor_map).
+
+Let tree_map_bij : bijective tree_map.
+Proof.
+by rewrite -setTT_bijective; have [? ? ?] := projT2 (cid cantor_map); split.
+Qed.
+
+#[local] HB.instance Definition _ := @BijTT.Build _ _ _ tree_map_bij.
+
+Lemma homeomorphism_cantor_like :
+  exists f : {splitbij [set: cantor_space] >-> [set: T]},
+    continuous f /\ (forall A, closed A -> closed (f @` A)).
+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.
+
+End TreeStructure.
+
+(* Part 3: Finitely branching trees are Cantor-like *)
+Section FinitelyBranchingTrees.
+Context {R : realType}.
+
+Definition tree_of (T : nat -> pointedType) : pseudoMetricType R :=
+  [the pseudoMetricType R of prod_topology
+    (fun n => pointed_discrete (T n))].
+
+Lemma cantor_like_finite_prod (T : nat -> topologicalType) :
+  (forall n, finite_set [set: pointed_discrete (T n)]) ->
+  (forall n, (exists xy : T n * T n, xy.1 != xy.2)) ->
+  cantor_like (tree_of T).
+Proof.
+move=> finiteT twoElems; split.
+- exact/(@perfect_diagonal (pointed_discrete \o T))/twoElems.
+- have := tychonoff (fun n => finite_compact (finiteT n)).
+  set A := (X in compact X -> _).
+  suff : A = [set: tree_of (fun x : nat => T x)] by move=> ->.
+  by rewrite eqEsubset.
+- apply: (@hausdorff_product _ (fun n => pointed_discrete (T n))) => n.
+  apply: discrete_hausdorff.
+  exact: discrete_pointed.
+- apply: zero_dimension_prod => ?.
+  apply: discrete_zero_dimension.
+  exact: discrete_pointed.
+Qed.
+
+End FinitelyBranchingTrees.
+
+Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope.
+
+(* Part 4: Building a finitely branching tree to cover `T` *)
+Section alexandroff_hausdorff.
+Context {R : realType} {T : pseudoMetricType R}.
+
+Hypothesis cptT : compact [set: T].
+Hypothesis hsdfT : hausdorff_space T.
+
+Section two_pointed.
+Context (t0 t1 : T).
+Hypothesis T2e : t0 != t1.
+
+Let ent_balls' (E : set (T * T)) :
+  exists M : set (set T), entourage E -> [/\
+    finite_set M,
+    forall A, M A -> exists a, A a /\
+      A `<=` closure [set y | split_ent E (a, y)],
+    exists A B : set T, M A /\ M B /\ A != B,
+    \bigcup_(A in M) A = [set: T] &
+    M `<=` closed].
+Proof.
+have [entE|?] := pselect (entourage E); last by exists point.
+move: cptT; rewrite compact_cover.
+pose fs x := interior [set y | split_ent E (x, y)].
+move=> /(_ T [ set: T] fs)[t _|t _ |].
+- exact: open_interior.
+- exists t => //.
+  by rewrite /fs /interior -nbhs_entourageE; exists (split_ent E).
+move=> M' _ Mcov; exists
+  ((closure \o fs) @` [set` M'] `|` [set [set t0]; [set t1]]).
+move=> _; split=> [|A [|]| | |].
+- rewrite finite_setU; split; first exact/finite_image/finite_fset.
+  exact: finite_set2.
+- move=> [z M'z] <-; exists z; split.
+  + apply: subset_closure; apply: nbhs_singleton; apply: nbhs_interior.
+    by rewrite -nbhs_entourageE; exists (split_ent E).
+  + by apply: closure_subset; exact: interior_subset.
+- by case => ->; [exists t0 | exists t1]; split => // t ->;
+    apply: subset_closure; exact: entourage_refl.
+- exists [set t0], [set t1]; split;[|split].
+  + by right; left.
+  + by right; right.
+  + apply/eqP; rewrite eqEsubset => -[] /(_ t0 erefl).
+    by move: T2e => /[swap] -> /eqP.
+- rewrite -subTset => t /Mcov [t' M't' fsxt]; exists (closure (fs t')).
+    by left; exists t'.
+  exact: subset_closure.
+- move=> ? [[? ?] <-|]; first exact: closed_closure.
+  by move=> [|] ->; exact/accessible_closed_set1/hausdorff_accessible.
+Qed.
+
+Let ent_balls E := projT1 (cid (ent_balls' E)).
+
+Let count_unif' := cid2
+  ((iffLR countable_uniformityP) (@countable_uniformity_metric _ T)).
+
+Let count_unif := projT1 count_unif'.
+
+Let ent_count_unif n : entourage (count_unif n).
+Proof.
+have := projT2 (cid (ent_balls' (count_unif n))).
+rewrite /count_unif; case: count_unif'.
+by move=> /= f fnA fnE; case /(_ (fnE _)) => _ _ _ + _; rewrite -subTset.
+Qed.
+
+Let count_unif_sub E : entourage E -> exists N, count_unif N `<=` E.
+Proof.
+by move=> entE; rewrite /count_unif; case: count_unif' => f + ? /=; exact.
+Qed.
+
+Let K' n : Type := @sigT (set T) (ent_balls (count_unif n)).
+
+Let K'p n : K' n.
+Proof.
+apply: cid; have [//| _ _ _ + _] := projT2 (cid (ent_balls' (count_unif n))).
+by rewrite -subTset => /(_ point I) [W Q ?]; exists W; exact: Q.
+Qed.
+
+HB.instance Definition _ n := gen_eqMixin (K' n).
+HB.instance Definition _ n := gen_choiceMixin (K' n).
+HB.instance Definition _ n := isPointed.Build (K' n) (K'p n).
+
+Let K n := [the pointedType of K' n].
+Let Tree := @tree_of R K.
+
+Let embed_refine n (U : set T) (k : K n) :=
+  (if pselect (projT1 k `&` U !=set0)
+  then projT1 k
+  else if pselect (exists e : K n , projT1 e `&` U !=set0) is left e
+    then projT1 (projT1 (cid e))
+    else set0) `&` U.
+Let embed_invar (U : set T) := closed U /\ U !=set0.
+
+Let Kn_closed n (e : K n) : closed (projT1 e).
+Proof.
+case: e => W; have [//| _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
+exact.
+Qed.
+
+Local Lemma cantor_surj_pt1 : exists2 f : Tree -> T,
+  continuous f & set_surj [set: Tree] [set: T] f.
+Proof.
+pose entn n := projT2 (cid (ent_balls' (count_unif n))).
+have [//| | |? []//| |? []// | |] := @tree_map_props (fun n => pointed_discrete (K n))
+    T (embed_refine) (embed_invar) cptT hsdfT.
+- by move=> n; exact: discrete_pointed.
+- move=> n U; rewrite eqEsubset; split=> [t Ut|t [? ? []]//].
+  have [//|_ _ _ + _] := entn n; rewrite -subTset.
+  move=> /(_ t I)[W cbW Wt]; exists (existT _ W cbW) => //.
+  by rewrite /embed_refine; case: pselect => //=; apply: absurd; exists t.
+- move=> n U e [clU Un0]; split.
+    apply: closedI => //; case: pselect => //= ?.
+    by case: pselect => ?; [exact: Kn_closed|exact: closed0].
+  rewrite /embed_refine; case: pselect => //= ?; case: pselect.
+    by case=> i [z [pz bz]]; set P := cid _; have := projT2 P; apply.
+  case: Un0 => z Uz; apply: absurd.
+  have [//|_ _ _ + _] := entn n; rewrite -subTset; move=> /(_ z I)[i bi iz].
+  by exists (existT _ _ bi), z.
+- by split; [exact: closedT | exists point].
+- move=> x y xny; move: hsdfT; rewrite open_hausdorff.
+  move=> /(_ _ _ xny)[[U V]] /= [/set_mem Ux /set_mem Vy] [+ oV UVI0].
+  rewrite openE => /(_ _ Ux); rewrite /interior -nbhs_entourageE => -[E entE ExU].
+  have [//| n ctE] :=
+    @count_unif_sub (split_ent E `&` (split_ent E)^-1%classic).
+    exact: filterI.
+  exists n => B [C ebC]; have [//|_ Csub _ _ _ embx emby] := entn n.
+  have [[D cbD] /= Dx Dy] : exists2 e : K n, projT1 e x & projT1 e y.
+    move: embx emby; rewrite /embed_refine; case: pselect => /=.
+      by move=> ? [? ?] [? ?]; exists (existT _ _ ebC).
+    case: pselect; last by move => ? ? [].
+    by move=> e _ [? ?] [? ?]; exists (projT1 (cid e)).
+  suff : E (x, y) by move/ExU; move/eqP/disjoints_subset: UVI0 => /[apply].
+  have [z [Dz DzE]] := Csub _ cbD.
+  have /ent_closure:= DzE _ Dx => /(_ (ent_count_unif n))/ctE [_ /= Exz].
+  have /ent_closure:= DzE _ Dy => /(_ (ent_count_unif n))/ctE [Ezy _].
+  exact: (@entourage_split _ (*[the uniformType of T]*) z).
+by move=> f [ctsf surjf _]; exists f.
+Qed.
+
+Local Lemma cantor_surj_pt2 :
+  exists f : {surj [set: cantor_space] >-> [set: Tree]}, continuous f.
+Proof.
+have [|f [ctsf _]] := @homeomorphism_cantor_like R Tree; last by exists f.
+apply: (@cantor_like_finite_prod _ (fun n => pointed_discrete (K n))) => [n /=|n].
+  have [//| fs _ _ _ _] := projT2 (cid (ent_balls' (count_unif n))).
+  suff -> : [set: {classic K' n}] =
+      (@projT1 (set T) _) @^-1` (projT1 (cid (ent_balls' (count_unif n)))).
+    by apply: finite_preimage => // ? ? _ _; exact: eq_sigT_hprop.
+  by rewrite eqEsubset; split => // -[].
+have [//| _ _ [A [B [pA [pB AB]]]] _ _] :=
+  projT2 (cid (ent_balls' (count_unif n))).
+exists (existT _ _ pA, existT _ _ pB) => /=.
+by move: AB; apply: contra_neq => -[].
+Qed.
+
+Local Lemma cantor_surj_twop :
+  exists f : {surj [set: cantor_space] >-> [set: T]}, continuous f.
+Proof.
+move: cantor_surj_pt2 cantor_surj_pt1 => -[f ctsf] [g ctsg /Psurj[sjg gsjg]].
+exists [surj of sjg \o f] => z.
+by apply continuous_comp; [exact: ctsf|rewrite -gsjg; exact: ctsg].
+Qed.
+
+End two_pointed.
+
+(* The Alexandroff-Hausdorff theorem*)
+Theorem cantor_surj :
+  exists f : {surj [set: cantor_space] >-> [set: T]}, continuous f.
+Proof.
+have [[p ppt]|/forallNP xpt] := pselect (exists p : T, p != point).
+  by apply: cantor_surj_twop; exact: ppt.
+have /Psurj[f cstf] : set_surj [set: cantor_space] [set: T] (cst point).
+  by move=> q _; exists point => //; have /negP/negPn/eqP -> := xpt q.
+by exists f; rewrite -cstf; exact: cst_continuous.
+Qed.
+
+End alexandroff_hausdorff.
diff --git a/theories/topology.v b/theories/topology.v
index 81c186bc7b..33602e38e9 100644
--- a/theories/topology.v
+++ b/theories/topology.v
@@ -3199,7 +3199,7 @@ Lemma compact_precompact (A B : set X) :
   hausdorff_space X -> compact A -> precompact A.
 Proof.
 move=> h c; rewrite precompactE ( _ : closure A = A)//.
-apply/esym/closure_id; exact: compact_closed.
+by apply/esym/closure_id; exact: compact_closed.
 Qed.
 
 Lemma precompact_closed (A : set X) : closed A -> precompact A = compact A.
@@ -3567,6 +3567,7 @@ Qed.
 Lemma close_eq x y : close x y -> x = y.
 Proof. by rewrite closeE. Qed.
 
+
 Lemma cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : T | F --> x].
 Proof. move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.
 
@@ -3656,7 +3657,7 @@ exists (fun i => if i is false then A `\` C else A `&` C); split.
   + rewrite setIC; apply/disjoints_subset; rewrite closureC => x [? ?].
     by exists C => //; split=> //; rewrite setDE setCI setCK; right.
   + apply/disjoints_subset => y -[Ay Cy].
-    rewrite -BAC BAD=> /closureI[_]; rewrite -(proj1 (@closure_id _ _) cD)=> Dy.
+    rewrite -BAC BAD => /closureI[_]; move/closure_id : cD => <- Dy.
     by have : B y; [by rewrite BAD; split|rewrite BAC => -[]].
 Qed.
 
@@ -3919,6 +3920,20 @@ rewrite /g ltnn /derange eq_sym; case: (eqVneq (f N) (distincts N).1) => //.
 by move=> ->; have := projT2 (sigW (npts N)).
 Qed.
 
+Lemma perfect_set2 {T} : perfect_set [set: T] <->
+  forall (U : set T), open U -> U !=set0 -> 
+  exists x y, [/\ U x, U y & x != y] .
+Proof.
+apply: iff_trans; first exact: perfectTP; split.
+  move=> nx1 U oU [] x Ux; exists x.
+  have : U <> [set x] by move=> Ux1; apply: (nx1 x); rewrite -Ux1.
+  apply: contra_notP; move/not_existsP/contrapT=> Uyx; rewrite eqEsubset.
+  (split => //; last by move=> ? ->); move=> y Uy; have  /not_and3P := Uyx y.
+  by case => // /negP; rewrite negbK => /eqP ->.
+move=> Unxy x Ox; have [] := Unxy _ Ox; first by exists x.
+by move=> y [] ? [->] -> /eqP.
+Qed.
+
 End perfect_sets.
 
 Section totally_disconnected.
@@ -5993,6 +6008,15 @@ pose B := \bigcup_n (f n) @` [set` h'' n]; exists B;[|split].
   by apply: (le_ball (ltW deleps)); apply: interior_subset.
 Qed.
 
+Lemma clopen_surj {R : realType} {T : pseudoMetricType R} :
+  compact [set: T] -> $|{surjfun [set: nat] >-> @clopen T}|.
+Proof.
+move=> cmptT.
+suff : @clopen T = set0 \/ $|{surjfun [set: nat] >-> @clopen T}|.
+  by case => //; rewrite eqEsubset => -[/(_ _ clopenT)].
+exact/pfcard_geP/clopen_countable/compact_second_countable.
+Qed.
+
 (* This section proves that uniform spaces, with a countable base for their
    entourage, are metrizable. The definition of this metric is rather arcane,
    and the proof is tough. That's ok because the resulting metric is not