From 2f4f02010bb4a17145b033b3dca764230cd10086 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 11 Nov 2022 23:04:21 -0500 Subject: [PATCH 1/4] fixing names --- theories/topology.v | 119 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 118 insertions(+), 1 deletion(-) diff --git a/theories/topology.v b/theories/topology.v index e02dc2b3f9..98c133c5ed 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3609,9 +3609,99 @@ 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, + forall A, B A -> open A & + 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_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} -> 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 : forall (x : T), exists (V : set T), D x -> B V /\ nbhs x V /\ V `<=` D. + move=> x; case: (pselect (D x)); last by move=> ?; exists set0. + by rewrite openE in oD; move=> /oD/Bbase [A[] ? [] ? ?]; exists A. +pose h' := fun 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. + +End ClopenSets. + (** * Uniform spaces *) Local Notation "A ^-1" := ([set xy | A (xy.2, xy.1)]) : classical_set_scope. @@ -4760,6 +4850,33 @@ 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. +have npos : forall n, ((0:R) < (n.+1%:R^-1))%R by []. +pose f : nat -> T -> (set T) := fun n z => (ball z (PosNum (npos n))%:num)^°. +move=> cmpt; have h : forall n, finSubCover [set: T] (f n) [set: T]. + move=> n; rewrite compact_cover in cmpt; apply: cmpt. + by move=> z _; rewrite /f; exact: open_interior. + by move=> z _; exists z => //; rewrite /f/interior; exact: nbhsx_ballx. +pose h' := fun n => (cid (iffLR (exists2P _ _) (h n))). +pose h'' := fun 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=> z [n _ [w wn <-]]; exact: open_interior. +- move=> x V /nbhs_ballP [] _/posnumP[eps] ballsubV. + have [//|N] := @ltr_add_invr R 0%R (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); split. + 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; apply: interior_subset. + by apply: (le_ball (ltW deleps)); apply: interior_subset. +Qed. + (** ** Complete uniform spaces *) Definition cauchy {T : uniformType} (F : set (set T)) := (F, F) --> entourage. From 3b9dd2bef50426b68f95521c606aa7166cc8bc65 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 11 Nov 2022 23:10:09 -0500 Subject: [PATCH 2/4] docs --- CHANGELOG_UNRELEASED.md | 5 +++++ theories/topology.v | 3 +++ 2 files changed, 8 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 00cc1182fb..a793952901 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -214,6 +214,11 @@ - 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`, and + `compact_second_countable`. ### Changed - in `topology.v` diff --git a/theories/topology.v b/theories/topology.v index 98c133c5ed..e194cc9acb 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 *) From 922d88ee0d4156f96a61a36a6313d11d6a78cdc9 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 11 Nov 2022 23:34:12 -0500 Subject: [PATCH 3/4] few helper lemmas --- CHANGELOG_UNRELEASED.md | 3 ++- theories/topology.v | 27 +++++++++++++++++++++++++-- 2 files changed, 27 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a793952901..e349063e1e 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -217,7 +217,8 @@ - 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`, and + `clopen_separatedP`, `totally_disconnected_cvg`, `clopen_countable`, + `totally_disconnected_prod`, `totally_disconnected_discrete`, and `compact_second_countable`. ### Changed diff --git a/theories/topology.v b/theories/topology.v index e194cc9acb..147e388f0e 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3624,7 +3624,7 @@ Implicit Types (T : topologicalType). Definition clopen {T} (A : set T) := open A /\ closed A. -Definition totally_disconnected {T} := forall (x y : T), +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). @@ -3642,6 +3642,10 @@ 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. @@ -3655,7 +3659,7 @@ by rewrite -[x in _ `<=` x]setCK. Qed. Lemma totally_disconnected_cvg {T} (x : T) : - {for x, totally_disconnected} -> compact [set: 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. @@ -3703,6 +3707,25 @@ rewrite eqEsubset; split => z. 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; apply/xneqy/functional_extensionality_dep. +exists ((prod_topo_apply i)@^-1` A); split;[|split] => //. +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 *) From 6c497a5dc1d32159785886a6f54acce69aea8ee7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 22 Nov 2022 21:47:13 +0900 Subject: [PATCH 4/4] linting (wip) --- theories/topology.v | 71 ++++++++++++++++++++++----------------------- 1 file changed, 35 insertions(+), 36 deletions(-) diff --git a/theories/topology.v b/theories/topology.v index 147e388f0e..7f97e7fdd2 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -3614,10 +3614,10 @@ 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, +Definition second_countable (T : topologicalType) := exists B, [/\ countable B, - forall A, B A -> open A & - forall (x:T) V, nbhs x V -> exists A, B A /\ nbhs x A /\ A `<=` V]. + B `<=` open & + forall (x : T) V, nbhs x V -> exists A, [/\ B A, nbhs x A & A `<=` V]]. Section ClopenSets. Implicit Types (T : topologicalType). @@ -3643,7 +3643,7 @@ 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). + 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). @@ -3683,20 +3683,20 @@ move=> /( _ _ _ (fun C y => ~ C y) (powerset_filter_from_filter PF)); case. by move=> D [] DF Dsub [C] DC /(_ _ DC) /subsetC2/filterS; apply; exact: DF. Qed. -Lemma clopen_countable {T} : +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. +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 : forall (x : T), exists (V : set T), D x -> B V /\ nbhs x V /\ V `<=` D. - move=> x; case: (pselect (D x)); last by move=> ?; exists set0. - by rewrite openE in oD; move=> /oD/Bbase [A[] ? [] ? ?]; exists A. -pose h' := fun z => projT1 (cid (h z)); have [] := @cmpt T D h'. +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. +- 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. @@ -3709,13 +3709,13 @@ Qed. Lemma totally_disconnected_prod (I : choiceType) (T : I -> topologicalType) : (forall i, @totally_disconnected (T i)) -> - (@totally_disconnected (product_topologicalType T)). + 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; apply/xneqy/functional_extensionality_dep. -exists ((prod_topo_apply i)@^-1` A); split;[|split] => //. -apply: clopen_comp => //; exact: prod_topo_apply_continuous. + 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} : @@ -4876,31 +4876,30 @@ 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} : +Lemma compact_second_countable {R : realType} {T : pseudoMetricType R} : compact [set: T] -> second_countable T. Proof. -have npos : forall n, ((0:R) < (n.+1%:R^-1))%R by []. -pose f : nat -> T -> (set T) := fun n z => (ball z (PosNum (npos n))%:num)^°. -move=> cmpt; have h : forall n, finSubCover [set: T] (f n) [set: T]. - move=> n; rewrite compact_cover in cmpt; apply: cmpt. - by move=> z _; rewrite /f; exact: open_interior. - by move=> z _; exists z => //; rewrite /f/interior; exact: nbhsx_ballx. -pose h' := fun n => (cid (iffLR (exists2P _ _) (h n))). -pose h'' := fun n => projT1 (h' n). -pose B := \bigcup_n (f n) @` [set` (h'' n)]; exists B; split. +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=> z [n _ [w wn <-]]; exact: open_interior. -- move=> x V /nbhs_ballP [] _/posnumP[eps] ballsubV. - have [//|N] := @ltr_add_invr R 0%R (eps%:num/2) _; rewrite add0r => deleps. - have [w [wh fx]] : exists w : T, w \in h'' N /\ f N w x. + 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); split. + 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; apply: interior_subset. - by apply: (le_ball (ltW deleps)); apply: interior_subset. + 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 *)