diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6ac6932cc0..3b0be23255 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -64,6 +64,12 @@ - in `measure.v`: + lemmas `ae_imply`, `ae_imply2` +- in file `topology.v`, + + new definitions `totally_disconnected`, and `zero_dimensional`. + + new lemmas `component_closed`, `zero_dimension_prod`, + `discrete_zero_dimension`, `zero_dimension_totally_disconnected`, + `totally_disconnected_cvg`, and `totally_disconnected_prod`. + ### Changed - in `mathcomp_extra.v` diff --git a/theories/topology.v b/theories/topology.v index 7ff5f328f8..1dcbd7e4f9 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -242,6 +242,11 @@ Require Import reals signed. (* component x == the connected component of point x *) (* perfect_set A == A is closed, and is every point in A *) (* is a limit point of A. *) +(* totally_disconnected A == The only connected subsets of A are *) +(* empty or singletons. *) +(* zero_dimensional T == Points are separable by a clopen set. *) +(* *) +(* *) (* [locally P] := forall a, A a -> G (within A (nbhs x)) *) (* if P is convertible to G (globally A) *) (* *) @@ -3645,6 +3650,18 @@ move=> Axy; apply/seteqP; split => z; apply: connected_component_trans => //. by apply: connected_component_sym. Qed. +Lemma component_closed A x : closed A -> closed (connected_component A x). +Proof. +move=> clA; have [Ax|Ax] := pselect (A x); first last. + by rewrite connected_component_out //; exact: closed0. +rewrite closure_id eqEsubset; split; first exact: subset_closure. +move=> z Axz; exists (closure (connected_component A x)) => //. +split; first exact/subset_closure/connected_component_refl. + rewrite [X in _ `<=` X](closure_id A).1//. + by apply: closure_subset; exact: connected_component_sub. +by apply: connected_closure; exact: component_connected. +Qed. + Lemma clopen_separatedP A : clopen A <-> separated A (~` A). Proof. split=> [[oA cA]|[] /[!(@disjoints_subset T)] /[!(@setCK T)] clAA AclA]. @@ -3767,6 +3784,70 @@ Qed. End perfect_sets. +Section totally_disconnected. +Implicit Types T : topologicalType. + +Definition totally_disconnected {T} (A : set T) := + forall x, A x -> connected_component A x = [set x]. + +Definition zero_dimensional T := + (forall x y, x != y -> exists U : set T, [/\ clopen U, U x & ~ U y]). + +Lemma zero_dimension_prod (I : choiceType) (T : I -> topologicalType) : + (forall i, zero_dimensional (T i)) -> + zero_dimensional (product_topologicalType T). +Proof. +move=> dctTI x y /eqP xneqy. +have [i/eqP/dctTI [U [clU Ux nUy]]] : exists i, x i <> y i. + by apply/existsNP=> W; exact/xneqy/functional_extensionality_dep. +exists (proj i @^-1` U); split => //; apply: clopen_comp => //. +exact/proj_continuous. +Qed. + +Lemma discrete_zero_dimension {T} : discrete_space T -> zero_dimensional T. +Proof. +move=> dctT x y xny; exists [set x]; split => //; last exact/nesym/eqP. +by split; [exact: discrete_open | exact: discrete_closed]. +Qed. + +Lemma zero_dimension_totally_disconnected {T} : + zero_dimensional T -> totally_disconnected [set: T]. +Proof. +move=> zdA x _; rewrite eqEsubset. +split=> [z [R [Rx _ ctdR Rz]]|_ ->]; last exact: connected_component_refl. +apply: contrapT => /eqP znx; have [U [[oU cU] Uz Ux]] := zdA _ _ znx. +suff : R `&` U = R by move: Rx => /[swap] <- []. +by apply: ctdR; [exists z|exists U|exists U]. +Qed. + +Lemma totally_disconnected_cvg {T : topologicalType} (x : T) : + hausdorff_space T -> zero_dimensional T -> compact [set: T] -> + filter_from [set D : set T | D x /\ clopen D] id --> x. +Proof. +pose F := filter_from [set D : set T | D x /\ clopen D] id. +have FF : Filter F. + apply: filter_from_filter; first by exists setT; split => //; exact: clopenT. + by move=> A B [? ?] [? ?]; exists (A `&` B) => //; split=> //; exact: clopenI. +have PF : ProperFilter F by apply: filter_from_proper; move=> ? [? _]; exists x. +move=> hsdfT zdT cmpT U Ux; rewrite nbhs_simpl -/F. +wlog oU : U Ux / open U. + move: Ux; rewrite /= nbhsE => -[] V [? ?] /filterS + /(_ V) P. + by apply; apply: P => //; exists V. +have /(iffLR (compact_near_coveringP _)) : compact (~` U). + by apply: (subclosed_compact _ cmpT) => //; exact: open_closedC. +move=> /(_ _ _ setC (powerset_filter_from_filter PF))[]. + move=> y nUy; have /zdT [C [[oC cC] Cx Cy]] : x != y. + by apply: contra_notN nUy => /eqP <-; exact: nbhs_singleton. + exists (~` C, [set U | U `<=` C]); first split. + - by apply: open_nbhs_nbhs; split => //; exact: closed_openC. + - apply/near_powerset_filter_fromP; first by move=> ? ?; exact: subset_trans. + by exists C => //; exists C. + - by case=> i j [? /subsetC]; apply. +by move=> D [DF _ [C DC]]/(_ _ DC)/subsetC2/filterS; apply; exact: DF. +Qed. + +End totally_disconnected. + (** * Uniform spaces *) Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. @@ -7235,6 +7316,22 @@ move/nbhs_singleton: nbhsU; move: x; apply/in_setP. by rewrite -continuous_open_subspace. Unshelve. end_near. Qed. +Lemma totally_disconnected_prod (I : choiceType) + (T : I -> topologicalType) (A : forall i, set (T i)) : + (forall i, totally_disconnected (A i)) -> + @totally_disconnected (product_topologicalType T) + (fun f => forall i, A i (f i)). +Proof. +move=> dsctAi x /= Aix; rewrite eqEsubset; split; last first. + by move=> ? ->; exact: connected_component_refl. +move=> f /= [C /= [Cx CA ctC Cf]]; apply/functional_extensionality_dep => i. +suff : proj i @` C `<=` [set x i] by apply; exists f. +rewrite -(dsctAi i) // => Ti ?; exists (proj i @` C) => //. +split; [by exists x | by move=> ? [r Cr <-]; exact: CA |]. +apply/(connected_continuous_connected ctC)/continuous_subspaceT. +exact: proj_continuous. +Qed. + Section UniformPointwise. Context {U : topologicalType} {V : uniformType}.