fix

CHANGELOG_UNRELEASED.md

@@ -4,72 +4,11 @@
 
 ### Added
 
-- file `Rstruct_topology.v`
-
-- package `coq-mathcomp-reals` depending on `coq-mathcomp-classical`
-  with files
-  + `constructive_ereal.v`
-  + `reals.v`
-  + `real_interval.v`
-  + `signed.v`
-  + `itv.v`
-  + `prodnormedzmodule.v`
-  + `nsatz_realtype.v`
-  + `all_reals.v`
-
-- in file `separation_axioms.v`,
-  + new lemmas `compact_normal_local`, and `compact_normal`.
-
-- package `coq-mathcomp-altreals` depending on `coq-mathcomp-reals`
-  with files
-  + `xfinmap.v`
-  + `discrete.v`
-  + `realseq.v`
-  + `realsum.v`
-  + `distr.v`
-
-- package `coq-mathcomp-reals-stdlib` depending on `coq-mathcomp-reals`
-  with file
-  + `Rstruct.v`
-
-- package `coq-mathcomp-analysis-stdlib` depending on
-  `coq-mathcomp-analysis` and `coq-mathcomp-reals-stdlib` with files
-  + `Rstruct_topology.v`
-  + `showcase/uniform_bigO.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`.
-
-- in file `mathcomp_extra.v`,
-  + new definition `sigT_fun`.
-- in file `sigT_topology.v`,
-  + new definition `sigT_nbhs`.
-  + new lemmas `sigT_nbhsE`, `existT_continuous`, `existT_open_map`,
-    `existT_nbhs`, `sigT_openP`, `sigT_continuous`, `sigT_setUE`, and 
-    `sigT_compact`.
-- in file `separation_axioms.v`,
-  + new lemma `sigT_hausdorff`.
+- in `num_topology.v`:
+  + lemma `in_continuous_mksetP`
 
 - in `normedtype.v`:
-  + lemma `in_continuous_mksetP`
-  + lemmas `continuous_within_itvcyP`, `continuous_within_itvycP`
+  + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP`
 
 ### Changed
 

theories/normedtype.v

@@ -8,7 +8,6 @@ From mathcomp Require Import cardinality set_interval ereal reals.
 From mathcomp Require Import signed topology prodnormedzmodule function_spaces.
 From mathcomp Require Export real_interval separation_axioms tvs.
 
-
 (**md**************************************************************************)
 (* # Norm-related Notions                                                     *)
 (*                                                                            *)
@@ -2158,14 +2157,6 @@ by apply: xe_A => //; rewrite eq_sym.
 Qed.
 Arguments cvg_at_leftE {R V} f x.
 
-(* TODO: move earlier *)
-Lemma in_continuous_mksetP {T : realFieldType} {U : realFieldType}
-    (i : interval T) (f : T -> U) :
-  {in i, continuous f} <-> {in [set` i], continuous f}.
-Proof.
-by split => [fi x /set_mem/=|fi x xi]; [exact: fi|apply: fi; rewrite inE].
-Qed.
-
 Section continuous_within_itvP.
 Context {R : realType}.
 Implicit Type f : R -> R.
@@ -2259,7 +2250,7 @@ rewrite bnd_simp/= le_eqVlt => /predU1P[<-{x}|ax] _.
   by move=> ?/=; rewrite !in_itv/= !andbT; exact: ltW.
 Qed.
 
-Lemma continuous_within_itvycP b (f : R -> R) :
+Lemma continuous_within_itvNycP b (f : R -> R) :
   {within `]-oo, b], continuous f} <->
   {in `]-oo, b[, continuous f} /\ f x @[x --> b^'-] --> f b.
 Proof.

theories/topology_theory/num_topology.v

@@ -90,6 +90,13 @@ End numFieldTopology.
 
 Import numFieldTopology.Exports.
 
+Lemma in_continuous_mksetP {T : realFieldType} {U : realFieldType}
+    (i : interval T) (f : T -> U) :
+  {in i, continuous f} <-> {in [set` i], continuous f}.
+Proof.
+by split => [fi x /set_mem/=|fi x xi]; [exact: fi|apply: fi; rewrite inE].
+Qed.
+
 Lemma nbhs0_ltW (R : realFieldType) (x : R) : (0 < x)%R ->
  \forall r \near nbhs (0%R:R), (r <= x)%R.
 Proof.