diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index fc923d98d..e769bc07a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -22,6 +22,27 @@ + `num_topology.v` + `quotient_topology.v` +- in file `separation_axioms.v`, + + new lemmas `compact_normal_local`, and `compact_normal`. + +- in file `topology_theory/one_point_compactification.v`, + + new definitions `one_point_compactification`, and `one_point_nbhs`. + + new lemmas `one_point_compactification_compact`, + `one_point_compactification_some_nbhs`, + `one_point_compactification_some_continuous`, + `one_point_compactification_open_some`, + `one_point_compactification_weak_topology`, and + `one_point_compactification_hausdorff`. + +- in file `normedtype.v`, + + new definition `type` (in module `completely_regular_uniformity`) + + new lemmas `normal_completely_regular`, + `one_point_compactification_completely_reg`, + `nbhs_one_point_compactification_weakE`, + `locally_compact_completely_regular`, and + `completely_regular_regular`. + + ### Changed - The file `topology.v` has been split into several files in the directory @@ -168,29 +189,6 @@ - moved from `topology.v` to `boolp.v`: + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP` -- in file `normedtype.v`, - + new definition `type` (in module `completely_regular_uniformity`) - + new lemmas `normal_completely_regular`, and - `locally_compact_completely_regular`. - + new definition `type`. - + new lemmas `normal_completely_regular`, - `one_point_compactification_completely_reg`, - `nbhs_one_point_compactification_weakE`, - `locally_compact_completely_regular`, and - `completely_regular_regular`. - -- in file `topology.v`, - + new definitions `one_point_compactification`, and `one_point_nbhs`. - + new lemmas `compact_normal_local`, and `compact_normal`. - + new lemmas `one_point_compactification_compact`, - `one_point_compactification_some_nbhs`, - `one_point_compactification_some_continuous`, - `one_point_compactification_open_some`, - `one_point_compactification_weak_topology`, and - `one_point_compactification_hausdorff`. -- in file `separation_axioms.v` - + new lemmas `compact_normal_local` and `compact_normal`. - ### Changed - in file `normedtype.v`, diff --git a/theories/normedtype.v b/theories/normedtype.v index d0fe993d5..5812211fd 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -3692,6 +3692,7 @@ Proof. exact: (normal_spaceP 0%N 1%N). Qed. End normalP. Section completely_regular. +Context {R : realType}. (**md This is equivalent to uniformizable. Note there is a subtle distinction between being uniformizable and being uniformType. @@ -3704,8 +3705,6 @@ Section completely_regular. Definition completely_regular_space (T : topologicalType) := forall (a : T) (B : set T), closed B -> ~ B a -> uniform_separator [set a] B. -(* Ideally, R should be an instance of realType here, - rather than a section variable. *) Lemma point_uniform_separator {T : uniformType} (x : T) (B : set T) : closed B -> ~ B x -> uniform_separator [set x] B. Proof. @@ -3719,13 +3718,7 @@ Qed. Lemma uniform_completely_regular {T : uniformType} : @completely_regular_space T. -<<<<<<< HEAD -Proof. -by move=> x B clB Bx; exact: point_uniform_separator. -Qed. -======= Proof. by move=> x B clB Bx; exact: point_uniform_separator. Qed. ->>>>>>> 4b77400b (just linting) Lemma normal_completely_regular {T : topologicalType} : normal_space T -> accessible_space T -> completely_regular_space T. @@ -3745,10 +3738,10 @@ End completely_regular. Module completely_regular_uniformity. Section completely_regular_uniformity. -Context {X : topologicalType}. +Context {R : realType} {X : topologicalType}. Hypothesis crs : completely_regular_space X. -Let X' : uniformType := @sup_topology X {f : X -> Rdefinitions.R | continuous f} +Let X' : uniformType := @sup_topology X {f : X -> R | continuous f} (fun f => Uniform.class (weak_topology (projT1 f))). Let completely_regular_nbhsE : @nbhs X X = nbhs_ (@entourage X'). @@ -3763,7 +3756,7 @@ move=> U; wlog oU : U / @open X U. move=> /[dup] nUx /nbhs_singleton Ux. have ufs : uniform_separator [set x] (~` U). by apply: crs; [exact: open_closedC | exact]. -have /uniform_separatorP := ufs => /(_ Rdefinitions.R)[f [ctsf f01 fx0 fU1]]. +have /uniform_separatorP := ufs => /(_ R)[f [ctsf f01 fx0 fU1]]. rewrite -nbhs_entourageE /entourage /= /sup_ent /= smallest_filter_finI. pose E := map_pair f @^-1` (fun pq => ball pq.1 1 pq.2). exists E; first last. @@ -3773,7 +3766,7 @@ exists E; first last. suff -> : f z = 1 by rewrite normr1 ltxx. by apply: fU1; exists z. move=> r /= [_]; apply => /=. -pose f' : {classic {f : X -> Rdefinitions.R | continuous f}} := exist _ f ctsf. +pose f' : {classic {f : X -> R | continuous f}} := exist _ f ctsf. suff /asboolP entE : @entourage (weak_topology f) (f', E).2. by exists (exist _ (f', E) entE). exists (fun pq => ball pq.1 1 pq.2) => //=. @@ -3807,18 +3800,19 @@ Hypothesis hsdf : hausdorff_space X. Let opc := @one_point_compactification X. -Lemma one_point_compactification_completely_reg : +Lemma one_point_compactification_completely_reg : completely_regular_space opc. Proof. -apply: normal_completely_regular. +apply: (@normal_completely_regular R). apply: compact_normal. exact: one_point_compactification_hausdorff. exact: one_point_compactification_compact. by apply: hausdorff_accessible; exact: one_point_compactification_hausdorff. Qed. + #[local] HB.instance Definition _ := Uniform.copy opc - (completely_regular_uniformity.type + (@completely_regular_uniformity.type R _ one_point_compactification_completely_reg). Let X' := @weak_topology X opc Some. @@ -3840,11 +3834,11 @@ Proof. exact: uniform_completely_regular. Qed. End locally_compact_uniform. -Lemma completely_regular_regular {X : topologicalType} : +Lemma completely_regular_regular {R : realType} {X : topologicalType} : completely_regular_space X -> @regular_space X. Proof. -move=> crsX; pose P' := completely_regular_uniformity.type crsX. -exact: @uniform_regular P'. +move=> crsX; pose P' := @completely_regular_uniformity.type R _ crsX. +exact: (@uniform_regular P'). Qed. Section pseudometric_normal. diff --git a/theories/topology_theory/one_point_compactification.v b/theories/topology_theory/one_point_compactification.v index 1dbe7ed30..f5bf89221 100644 --- a/theories/topology_theory/one_point_compactification.v +++ b/theories/topology_theory/one_point_compactification.v @@ -1,7 +1,7 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect all_algebra all_classical. From mathcomp Require Import signed topology_structure uniform_structure. -From mathcomp Require Import pseudometric_structure compact. +From mathcomp Require Import pseudometric_structure compact weak_topology. (**md**************************************************************************) (* # One Point Compactifications *) @@ -14,6 +14,10 @@ From mathcomp Require Import pseudometric_structure compact. (* as an alias of `option X` *) (******************************************************************************) +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + + Definition one_point_compactification (X : Type) : Type := option X. Section one_point_compactification. @@ -63,7 +67,7 @@ HB.instance Definition _ := hasNbhs.Build opc one_point_nbhs. HB.instance Definition _ := @Nbhs_isNbhsTopological.Build opc one_point_filter one_point_singleton one_point_nbhs_nbhs. -Lemma opc_compact : compact [set: opc]. +Lemma one_point_compactification_compact : compact [set: opc]. Proof. apply/compact_near_coveringP => ? F /= P FF FT. have [//| [U i [[W /= [cptW cW WU nfI UIP]]]]] := FT None. @@ -81,29 +85,30 @@ move=> ?; apply: (UIP (Some z,j)); split => //=. exact: (near nfI _). Unshelve. all: by end_near. Qed. -Lemma opc_some_nbhs (x : X) (U : set X) : +Lemma one_point_compactification_some_nbhs (x : X) (U : set X) : nbhs x U -> @nbhs _ opc (Some x) (Some @` U). Proof. rewrite {2}/nbhs /= nbhs_simpl /= => /filterS; apply; exact: preimage_image. Qed. -Lemma opc_some_continuous : continuous (Some : X -> opc). +Lemma one_point_compactification_some_continuous : continuous (Some : X -> opc). Proof. by move=> x U. Qed. -Lemma opc_open_some (U : set X) : open U -> @open opc (Some @` U). +Lemma one_point_compactification_open_some (U : set X) : + open U -> @open opc (Some @` U). Proof. rewrite ?openE /= => Uo ? /= [x /[swap] <- Ux] /=. -by apply: opc_some_nbhs; apply: Uo. +by apply: one_point_compactification_some_nbhs; apply: Uo. Qed. -Lemma opc_weak_topology : +Lemma one_point_compactification_weak_topology : @nbhs _ (@weak_topology X opc Some) = @nbhs _ X. Proof. rewrite funeq2E=> x U; apply/propeqP; split; rewrite /(@nbhs _ (weak_topology _)) /=. - case => V [[/= W] oW <- /= Ws] /filterS; apply; apply: opc_some_continuous. - exact: oW. + case => V [[/= W] oW <- /= Ws] /filterS; apply. + by apply: one_point_compactification_some_continuous; exact: oW. rewrite nbhsE; case => V [? ? ?]; exists V; split => //. -exists (Some @` V); first exact: opc_open_some. +exists (Some @` V); first exact: one_point_compactification_open_some. rewrite eqEsubset; split => z /=; first by case=> ? /[swap] /Some_inj ->. by move=> ?; exists z. Qed.