Splitting Topology part 3: Separation axioms

CHANGELOG_UNRELEASED.md

@@ -168,7 +168,29 @@
 - moved from `topology.v` to `boolp.v`:
   + lemmas `bigmax_geP`, `bigmax_gtP`, `bigmin_leP`, `bigmin_ltP`
 
+- moved from `topology.v` to `separation_axioms.v`: `set_nbhs`, `set_nbhsP`,
+    `accessible_space`, `kolmogorov_space`, `hausdorff_space`,
+    `compact_closed`, `discrete_hausdorff`, `compact_cluster_set1`,
+    `compact_precompact`, `open_hausdorff`, `hausdorff_accessible`,
+    `accessible_closed_set1`, `accessible_kolmogorov`,
+    `accessible_finite_set_closed`, `subspace_hausdorff`, `order_hausdorff`,
+    `ball_hausdorff`, `Rhausdorff`, `close`, `closeEnbhs`, `closeEonbhs`,
+    `close_sym`, `cvg_close`, `close_refl`, `cvgx_close`, `cvgi_close`,
+    `cvg_toi_locally_close`, `closeE`, `close_eq`, `cvg_unique`, `cvg_eq`,
+    `cvgi_unique`, `close_cvg`, `lim_id`, `lim_near_cst`, `lim_cst`,
+    `entourage_close`, `close_trans`, `close_cvgxx`, `cvg_closeP`,
+    `ball_close`, `normal_space`, `regular_space`, `compact_regular`,
+    `uniform_regular`, `totally_disconnected`, `zero_dimensional`,
+    `discrete_zero_dimension`, `zero_dimension_totally_disconnected`,
+    `zero_dimensional_ray`, `type`, `countable_uniform_bounded`,
+    `countable_uniform`, `sup_pseudometric`, `countable_uniformityT`, `gauge`,
+    `iter_split_ent`, `gauge_ent`, `gauge_filter`, `gauge_refl`, `gauge_inv`,
+    `gauge_split`, `gauge_countable_uniformity`, `uniform_pseudometric_sup`,
+    `perfect_set`, `perfectTP`, and `perfect_set2`.
 ### Renamed
+- in file `topology.v` -> `separation_axioms.v`
+  + `totally_disconnected_cvg` -> `zero_dimensional_cvg`.
+
 
 ### Generalized
 

_CoqProject

@@ -27,6 +27,7 @@ theories/reals.v
 theories/landau.v
 theories/Rstruct.v
 theories/topology.v
+theories/separation_axioms.v
 theories/function_spaces.v
 theories/cantor.v
 theories/prodnormedzmodule.v

theories/Make

@@ -13,6 +13,7 @@ reals.v
 landau.v
 Rstruct.v
 topology.v
+separation_axioms.v
 function_spaces.v
 cantor.v
 prodnormedzmodule.v

theories/cantor.v

@@ -1,10 +1,10 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum interval rat.
 From mathcomp Require Import finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality.
-From mathcomp Require Import reals signed topology function_spaces.
-From HB Require Import structures.
+Require Import reals signed topology function_spaces separation_axioms.
 
 (**md**************************************************************************)
 (* # The Cantor Space and Applications                                        *)

theories/function_spaces.v

@@ -3,7 +3,7 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
-Require Import reals signed topology.
+Require Import reals signed topology separation_axioms.
 
 (**md**************************************************************************)
 (* # The topology of functions spaces                                         *)
@@ -1421,7 +1421,7 @@ Lemma continuous_uncurry (f : U -> V -> W) :
 Proof.
 move=> lcV hsdf ctsf cf; apply: continuous_uncurry_regular => //.
 move=> v; have [B] := @lcV v I; rewrite withinET => Bv [cptB clB].
-by move=> z; exact: (@compact_regular V hsdf v B).
+by move=> z; exact: (compact_regular _ cptB).
 Qed.
 
 Lemma curry_continuous (f : (U * V)%type -> W) : continuous f -> @regular_space U ->

theories/normedtype.v

@@ -6,6 +6,7 @@ From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import cardinality set_interval Rstruct.
 Require Import ereal reals signed topology prodnormedzmodule function_spaces.
+Require Export separation_axioms.
 
 (**md**************************************************************************)
 (* # Norm-related Notions                                                     *)