some linting and changelog

CHANGELOG_UNRELEASED.md

@@ -120,6 +120,13 @@
   + new definition `normal_space`.
   + new lemmas `filter_inv`, and `countable_uniform_bounded`.
 
+- in file `normedtype.v`,
+  + new lemmas `normal_openP`, `normal_separatorP`, `uniform_regular`, 
+    `regular_openP`, and `pseudometric_normal`.
+- in file `topology.v`,
+  + new definition `regular_space`.
+  + new lemma `ent_closure`.
+
 
 ### Changed
 
@@ -215,6 +222,8 @@
 
 - in `normedtype.v`:
   + `nbhs_closedballP` -> `nbhs_closed_ballP`
+- in `normedtype.v`: 
+  + `normal_urysohnP` -> `normal_separatorP`.
 
 ### Generalized
 

theories/normedtype.v

@@ -4198,7 +4198,7 @@ Let normal_spaceP : [<->
 ].
 Proof.
 tfae; first by move=> *; exact: normal_uniform_separator.
-- move=> + A B clA clB AB0 => /(_ _ _ clA clB AB0) /(@uniform_separatorP _ R). 
+- move=> + A B clA clB AB0 => /(_ _ _ clA clB AB0) /(@uniform_separatorP _ R).
   case=> f [cf f01 /imsub1P/subset_trans fa0 /imsub1P/subset_trans fb1]. 
   exists (f@^-1` `]-1, 1/2[), (f@^-1` `]1/2, 2[); split.
   + by apply: open_comp; [|exact: interval_open] => + _ .
@@ -4231,45 +4231,27 @@ Lemma normal_separatorP : normal_space T <->
 Proof. exact: (normal_spaceP 0%N 1%N). Qed.
 End normalP.
 
-Section normal_separations.
-
-Local Notation "'to_set' A x" := [set y | A (x, y)]
-  (at level 0, A at level 0) : classical_set_scope.
-Local Notation "A ^-1" := [set xy | A (xy.2, xy.1)] : classical_set_scope.
-
-Lemma ent_closure {X : uniformType} (x : X) E : entourage E ->
-  closure (to_set (split_ent E) x) `<=` to_set E x.
-Proof.
-pose E' := ((split_ent E) `&` ((split_ent E)^-1)%classic).
-move=> entE z /(_ [set y | E' (z, y)]) [].
-  by rewrite -nbhs_entourageE; exists E' => //; apply: filterI.
-by move=> y [/=] + [_]; apply: entourage_split.
-Qed.
-
-Definition regular_space (T : topologicalType) :=
-  forall (a : T), nbhs a `<=` filter_from (nbhs a) closure.
-
-Lemma uniform_regular {X : uniformType} (x : X) : {for x, @regular_space X}.
+Section pseudometric_normal.
+Lemma uniform_regular {X : uniformType} : @regular_space X.
 Proof.
-move=> A /=.
-rewrite -nbhs_entourageE; case => E entE /(subset_trans (ent_closure entE)) ?.
-by exists (to_set (split_ent E) x); first by exists (split_ent E).
+move=> x A; rewrite /= -nbhs_entourageE; case => E entE.
+move/(subset_trans (ent_closure entE)) => ?.
+by exists [set y | (split_ent E) (x, y)]; first by exists (split_ent E).
 Qed.
 
-Lemma regularP {T : topologicalType} (x : T) : 
+Lemma regular_openP {T : topologicalType} (x : T) : 
   {for x, @regular_space T} <-> (forall A, closed A -> ~ A x -> exists (U V : set T),
     [/\ open U, open V, U x, A `<=` V & U `&` V = set0]).
 Proof.
 split.
   move=> + A clA nAx => /(_ (~` A)) [].
     by apply: open_nbhs_nbhs; split => //; apply: closed_openC.
   move=> U Ux /subsetC; rewrite setCK => AclU; exists (interior U). 
-  exists (~` (closure U)); split => //.
-  - by apply: open_interior.
-  - by apply: closed_openC; exact: closed_closure.
-  - apply/disjoints_subset; rewrite setCK; apply: (@subset_trans _ U).
-      exact: interior_subset.
-    exact: subset_closure.
+  exists (~` (closure U)); split => //; first exact: open_interior.
+    by apply: closed_openC; exact: closed_closure.
+  apply/disjoints_subset; rewrite setCK; apply: (@subset_trans _ U).
+    exact: interior_subset.
+  exact: subset_closure.
 move=> + A Ax => /(_ (~` (interior A))) []; [|exact|].
   by apply: open_closedC; exact: open_interior.
 move=> U [V] [oU oV Ux /subsetC cAV /disjoints_subset UV]; exists U.
@@ -4286,7 +4268,7 @@ apply/(@normal_openP _ R) => A B clA clB AB0.
 have eps' D : closed D -> forall (x:X), exists (eps : {posnum R}), ~ D x ->
     ball x eps%:num `&` D = set0.
   move=> clD x; case: (pselect (~ D x)); last by move => ?; exists 1%:pos.
-  move=> ndx; have /regularP/(_ _ clD) [//|] := @uniform_regular X x.
+  move=> ndx; have /regular_openP/(_ _ clD) [//|] := @uniform_regular X x.
   move=> U [V] [+ oV] Ux /subsetC BV /disjoints_subset UV0.
   rewrite openE /interior => /(_ _ Ux); rewrite -nbhs_ballE; case.
   move => _/posnumP[eps] beU; exists eps => _; apply/disjoints_subset.
@@ -4313,7 +4295,7 @@ move/ball_sym:Bye =>/[swap] /le_ball /[apply] /(ball_triangle Axe).
 rewrite -splitr => byx; have := projT2 (cid (eps' _ clB x)) nBx.
 by rewrite -subset0; apply; split; first exact: byx.
 Qed.
-End normal_separations.
+End pseudometric_normal.
 
 Section open_closed_sets_ereal.
 Variable R : realFieldType (* TODO: generalize to numFieldType? *).

theories/topology.v

@@ -118,6 +118,7 @@ Require Import reals signed.
 (*                                     eventually true.                       *)
 (*                         clopen U == U is both open and closed              *)
 (*                   normal_space X == X is normal, sometimes called T4       *)
+(*                  regular_space X == X is regular, sometimes called T3      *)
 (*    separate_points_from_closed f == For a closed set U and point x outside *)
 (*                                     some member of the family f sends      *)
 (*                                     f_i(x) outside (closure (f_i @` U)).   *)
@@ -4259,6 +4260,15 @@ Arguments entourage_split {M} z {x y A}.
 #[global]
 Hint Extern 0 (nbhs _ (to_set _ _)) => exact: nbhs_entourage : core.
 
+Lemma ent_closure {M : uniformType} (x : M) E : entourage E ->
+  closure (to_set (split_ent E) x) `<=` to_set E x.
+Proof.
+pose E' := ((split_ent E) `&` ((split_ent E)^-1)%classic).
+move=> entE z /(_ [set y | E' (z, y)]) [].
+  by rewrite -nbhs_entourageE; exists E' => //; apply: filterI.
+by move=> y [/=] + [_]; apply: entourage_split.
+Qed.
+
 Lemma continuous_withinNx {U V : uniformType} (f : U -> V) x :
   {for x, continuous f} <-> f @ x^' --> f x.
 Proof.
@@ -7797,6 +7807,9 @@ Definition normal_space (T : topologicalType) :=
   forall (A : set T), closed A ->
     set_nbhs A `<=` filter_from (set_nbhs A) closure.
 
+Definition regular_space (T : topologicalType) :=
+  forall (a : T), nbhs a `<=` filter_from (nbhs a) closure.
+
 Section ArzelaAscoli.
 Context {X : topologicalType}.
 Context {Y : uniformType}.