From c518e2a302126cbc96a7527e28cac28aaf443822 Mon Sep 17 00:00:00 2001 From: zstone1 Date: Tue, 14 Nov 2023 11:05:15 -0500 Subject: [PATCH] Alexandroff-Hausdorff Theorem and the Cantor Space (#834) -- Co-authored-by: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Co-authored-by: Reynald Affeldt --- CHANGELOG_UNRELEASED.md | 12 + _CoqProject | 1 + theories/cantor.v | 542 ++++++++++++++++++++++++++++++++++++++++ theories/topology.v | 29 ++- 4 files changed, 582 insertions(+), 2 deletions(-) create mode 100644 theories/cantor.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 971b02c98..e2709956a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -4,6 +4,18 @@ ### 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` + ### Changed ### Renamed diff --git a/_CoqProject b/_CoqProject index fb6175469..fcb3ccc19 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 000000000..db97c04a3 --- /dev/null +++ b/theories/cantor.v @@ -0,0 +1,542 @@ +(* 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 cantor_space := + product_uniformType (fun _ : nat => @discrete_uniformType _ discrete_bool). + +Definition cantor_like (T : topologicalType) := + [/\ perfect_set [set: T], + compact [set: T], + hausdorff_space T & + zero_dimensional T]. + +Canonical cantor_pseudoMetric {R} := + @product_pseudoMetricType R _ (fun _ : nat => + @discrete_pseudoMetricType R _ discrete_bool) (countableP _). + +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. by apply: hausdorff_product => ?; exact: discrete_hausdorff. Qed. + +Lemma cantor_zero_dimensional : zero_dimensional cantor_space. +Proof. by apply: zero_dimension_prod => _; exact: discrete_zero_dimension. 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 := product_topologicalType 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=> [topologicalType of bool]) T c_ind c_invar cmptT hsdfT. +- by []. +- 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 pointed_discrete (P : pointedType) : pseudoMetricType R := + @discrete_pseudoMetricType R + (@discrete_uniformType (TopologicalType + (FilteredType P P principal_filter) + discrete_topological_mixin) + erefl) erefl. + +Definition tree_of (T : nat -> pointedType) : pseudoMetricType R := + @product_pseudoMetricType R _ + (fun n => pointed_discrete (T n)) + (countableP _). + +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)). + by congr (compact _) => //=; rewrite eqEsubset. +- apply: (@hausdorff_product _ (pointed_discrete \o T)) => n. + exact: discrete_hausdorff. +- by apply zero_dimension_prod => ?; exact: discrete_zero_dimension. +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. + +Let K n := PointedType (classicType_choiceType (K' n)) (K'p 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 (@pointed_discrete R \o K) + T (embed_refine) (embed_invar) cptT hsdfT. +- 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 [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 _ (@pointed_discrete R \o K)) => [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 cacc5acc0..9eed00f36 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3221,7 +3221,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. @@ -3586,6 +3586,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. @@ -3675,7 +3676,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. @@ -3942,6 +3943,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. @@ -5270,6 +5285,7 @@ Qed. Definition prod_pseudoMetricType_mixin := PseudoMetric.Mixin prod_ball_center prod_ball_sym prod_ball_triangle prod_entourage. End prod_PseudoMetric. + Canonical prod_pseudoMetricType (R : numDomainType) (U V : pseudoMetricType R) := PseudoMetricType (U * V) (@prod_pseudoMetricType_mixin R U V). @@ -6599,6 +6615,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