diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 00cc1182fb..e349063e1e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -214,6 +214,12 @@ - in file `topology.v`, + new lemmas `dfwith_continuous`, and `proj_open`. +- in file `topology.v`, + + new definitions `second_countable`, `clopen`, and `totally_disconnected`. + + new lemmas `clopenI`, `clopenU`, `clopenC`, `clopen0`, `clopenT`, + `clopen_separatedP`, `totally_disconnected_cvg`, `clopen_countable`, + `totally_disconnected_prod`, `totally_disconnected_discrete`, and + `compact_second_countable`. ### Changed - in `topology.v` diff --git a/theories/topology.v b/theories/topology.v index e02dc2b3f9..7f97e7fdd2 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -230,6 +230,9 @@ Require Import reals signed. (* component x == the connected component of point x *) (* [locally P] := forall a, A a -> G (within A (nbhs x)) *) (* if P is convertible to G (globally A) *) +(* second_countable T == T has a countable basis *) +(* clopen A == A is both open and closed *) +(* totally_disconnected A == distinct points are separated *) (* *) (* * Function space topologies : *) (* {uniform` A -> V} == The space U -> V, equipped with the topology of *) @@ -3609,9 +3612,122 @@ Lemma bool_compact : compact [set: bool]. Proof. by rewrite setT_bool; apply/compactU; exact: compact_set1. Qed. End DiscreteTopology. - #[global] Hint Resolve discrete_bool : core. +Definition second_countable (T : topologicalType) := exists B, + [/\ countable B, + B `<=` open & + forall (x : T) V, nbhs x V -> exists A, [/\ B A, nbhs x A & A `<=` V]]. + +Section ClopenSets. +Implicit Types (T : topologicalType). + +Definition clopen {T} (A : set T) := open A /\ closed A. + +Definition totally_disconnected T := forall (x y : T), + x != y -> exists A, A x /\ ~ A y /\ clopen A. + +Lemma clopenI {T} (A B : set T) : clopen A -> clopen B -> clopen (A `&` B). +Proof. by case=> ? ? [] ? ?; split; [exact: openI | exact: closedI]. Qed. + +Lemma clopenU {T} (A B : set T) : clopen A -> clopen B -> clopen (A `|` B). +Proof. by case=> ? ? [] ? ?; split; [exact: openU | exact: closedU]. Qed. + +Lemma clopenC {T} (A B : set T) : clopen A -> clopen (~`A). +Proof. by case=> ? ?; split;[exact: closed_openC | exact: open_closedC ]. Qed. + +Lemma clopen0 {T} : @clopen T set0. +Proof. by split; [exact: open0 | exact: closed0]. Qed. + +Lemma clopenT {T} : clopen [set: T]. +Proof. by split; [exact: openT | exact: closedT]. Qed. + +Lemma clopen_comp {T U : topologicalType} (f : T -> U) (A : set U) : + clopen A -> continuous f -> clopen (f @^-1` A). +Proof. by case=> ? ?; split; [ exact: open_comp | exact: closed_comp]. Qed. + +Lemma clopen_separatedP {T} (A : set T) : clopen A <-> separated A (~` A). +Proof. +split. + case=> oA cA; rewrite /separated -((closure_id A).1 cA) setICr; split => //. + by rewrite -((closure_id _).1 (open_closedC oA)) setICr. +case; rewrite ?disjoints_subset => clAA AclA; split. + rewrite -closedC closure_id eqEsubset; split; first exact: subset_closure. + exact: subsetCr. +rewrite closure_id eqEsubset; split => //; first exact: subset_closure. +by rewrite -[x in _ `<=` x]setCK. +Qed. + +Lemma totally_disconnected_cvg {T} (x : T) : + {for x, totally_disconnected T} -> compact [set: T] -> + filter_from [set D | D x /\ clopen D] id --> x. +Proof. +pose F := filter_from [set D | D x /\ clopen D] id. +have PF : ProperFilter F. + apply: filter_from_proper; first apply: filter_from_filter. + - by exists setT; split => //; exact: clopenT. + - move=> A B [] ? ? [] ? ?; exists (A `&` B); [split |] => //; exact: clopenI. + - by move=> ? [? _]; exists x. +move=> disct cmpT U Ux; rewrite nbhs_simpl -/F; wlog oU : U Ux / open U. + move: Ux; rewrite /= {1}nbhsE => [][] O [] Ox OsubU P; apply: (filterS OsubU). + by apply: P => //; [exact: open_nbhs_nbhs | case: Ox]. +have /compact_near_coveringP.1 : compact (~`U). + by apply: (subclosed_compact _ cmpT) => //; exact: open_closedC. +move=> /( _ _ _ (fun C y => ~ C y) (powerset_filter_from_filter PF)); case. + move=> y nUy; have /disct [C [Cx [] ? [] ? ?]] : x != y. + by apply/eqP => E; move: nUy; rewrite -E; apply; apply: nbhs_singleton. + exists (~`C, [set U | U `<=` C]); last by move=> [? ?] [? /subsetC]; exact. + split; first 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 move=> D [] DF Dsub [C] DC /(_ _ DC) /subsetC2/filterS; apply; exact: DF. +Qed. + +Lemma clopen_countable {T} : + compact [set: T] -> second_countable T -> countable (@clopen T). +Proof. +move=> cmpT [B []] /fset_subset_countable cntB obase Bbase. +apply/(card_le_trans _ cntB)/pcard_surjP. +pose f := fun (F : {fset set T}) => \bigcup_(x in [set` F]) x; exists f. +move=> D [] oD cD /=; have cmpt : cover_compact D. + by rewrite -compact_cover; exact: (subclosed_compact _ cmpT). +have h (x : T) : exists (V : set T), D x -> B V /\ nbhs x V /\ V `<=` D. + case: (pselect (D x)); last by move=> ?; exists set0. + by rewrite openE in oD => /oD/Bbase [A[] ? ? ?]; exists A. +pose h' z := projT1 (cid (h z)); have [] := @cmpt T D h'. +- by move=> z Dz; apply: obase; have [] := projT2 (cid (h z)) Dz. +- move=> z Dz; exists z => //; apply: nbhs_singleton. + by have [? []] := projT2 (cid (h z)) Dz. +move=> fs fsD DsubC; exists ([fset h' z | z in fs])%fset. + move=> U/imfsetP [z] /fsD /set_mem Dz ->; rewrite inE. + by have [? []] := projT2 (cid (h z)) Dz. +rewrite eqEsubset; split => z. + case=> y /imfsetP [x /fsD/set_mem Dx ->]; move: z. + by have [? []] := projT2 (cid (h x)) Dx. +by move=> /DsubC [y yfs hyz]; exists (h' y) => //; rewrite set_imfset; exists y. +Qed. + +Lemma totally_disconnected_prod (I : choiceType) (T : I -> topologicalType) : + (forall i, @totally_disconnected (T i)) -> + totally_disconnected (product_topologicalType T). +Proof. +move=> dctTI /= x y /eqP xneqy. +have [i /eqP /dctTI [A] [] Axi [] nAy coA] : exists i, x i <> y i. + by apply/existsNP=> W; exact/xneqy/functional_extensionality_dep. +exists (prod_topo_apply i @^-1` A); split;[|split] => //. +by apply: clopen_comp => //; exact: prod_topo_apply_continuous. +Qed. + +Lemma totally_disconnected_discrete {T} : + discrete_space T -> totally_disconnected T. +Proof. +move=> dsct x y /eqP xneqy; exists [set x]; split; [|split] => //. + by move=> W; apply: xneqy; rewrite W. +by split => //; [exact: discrete_open | exact: discrete_closed]. +Qed. + +End ClopenSets. + (** * Uniform spaces *) Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. @@ -4760,6 +4876,32 @@ Definition fct_pseudoMetricType_mixin := Canonical fct_pseudoMetricType := PseudoMetricType (T -> U) fct_pseudoMetricType_mixin. End fct_PseudoMetric. +Lemma compact_second_countable {R : realType} {T : pseudoMetricType R} : + compact [set: T] -> second_countable T. +Proof. +pose f n z : set T := (ball z n.+1%:R^-1)^°. +move=> cmpt; have h n : finSubCover [set: T] (f n) [set: T]. + move: cmpt; rewrite compact_cover; apply. + by move=> z _; exact: open_interior. + by move=> z _; exists z => //; exact: (nbhsx_ballx _ n.+1%:R^-1%:pos). +pose h' n := cid (iffLR (exists2P _ _) (h n)). +pose h'' n := projT1 (h' n). +pose B := \bigcup_n (f n) @` [set` h'' n]; exists B; split. +- apply: bigcup_countable => // n _; apply: finite_set_countable. + exact/finite_image/finite_fset. +- by move=> _ [n _ [w wn <-]]; exact: open_interior. +- move=> x V /nbhs_ballP[] _/posnumP[eps] ballsubV. + have [//|N] := @ltr_add_invr R 0 (eps%:num / 2) _; rewrite add0r => deleps. + have [w [wh fx]] : exists w : T, w \in h'' N /\ f N w x. + by have [_ /(_ x) [// | w ? ?]] := projT2 (h' N); exists w. + exists (f N w); split; first by exists N. + by apply: open_nbhs_nbhs; split => //; exact: open_interior. + apply: subset_trans ballsubV => z bz. + rewrite [_%:num]splitr; apply: (@ball_triangle _ _ w). + by apply: (le_ball (ltW deleps)); apply/ball_sym; exact: interior_subset. + by apply: (le_ball (ltW deleps)); exact: interior_subset. +Qed. + (** ** Complete uniform spaces *) Definition cauchy {T : uniformType} (F : set (set T)) := (F, F) --> entourage.