fixing build

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`,

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.

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.