formatting

- `setC_subset_set1C` rename to `mem_setC_subset` on the model
   of the lemma `disjoints_subset`
- `setC1E` rather than `set1CE` with equality the other way around
- rename `T_0` and `T_1` to `kolmogorov` and `accessible` on
  the model of `hausdorff`
- update changelog and documentation

CHANGELOG_UNRELEASED.md

@@ -47,6 +47,11 @@
 - in `normedtype.v`:
   + lemmas `ereal_is_cvgN`, `ereal_cvgZr`, `ereal_is_cvgZr`, `ereal_cvgZl`, `ereal_is_cvgZl`,
     `ereal_limZr`, `ereal_limZl`, `ereal_limN`
+- in `classical_sets.v`:
+  + lemmas `setC1E`, `mem_setC_subset`
+- in `topology.v`:
+  + definitions `kolmogorov`, `accessible`
+  + lemmas `accessible_closed_set1`, `accessible_kolmogorov`
 
 ### Changed
 

theories/classical_sets.v

@@ -335,7 +335,10 @@ Proof. by rewrite subsets_disjoint setCK. Qed.
 
 Lemma setCT : ~` setT = set0 :> set T. Proof. by rewrite -setC0 setCK. Qed.
 
-Lemma set1CE (x : T) : [set y | y <> x] = [set~ x]. Proof. by []. Qed.
+Lemma setC1E (x : T) : [set ~ x] = [set y | y <> x]. Proof. by []. Qed.
+
+Lemma mem_setC_subset (x : T) A : x \in ~` A -> A `<=` [set ~ x].
+Proof. by rewrite in_setE => + y Ay; apply: contra_not => <-. Qed.
 
 Lemma setDE A B : A `\` B = A `&` ~` B. Proof. by []. Qed.
 
@@ -458,14 +461,6 @@ Proof. by rewrite predeqE => ?; split => // -[]. Qed.
 Lemma setICr A : A `&` ~` A = set0.
 Proof. by rewrite setIC setICl. Qed.
 
-Lemma setC_subset_set1C (x : T) (A : set T) : x \in ~` A -> A `<=` [set ~ x].
-Proof.
-  rewrite in_setE /set1 => ? y yInH //= ; rewrite /setC => //= xEqy.
-  have: (A `&` ~` A) y.
-     rewrite /setI => //= ; split; by [rewrite xEqy|].
-  by rewrite setICr.
-Qed.
-
 Lemma setIA A B C : A `&` (B `&` C) = A `&` B `&` C.
 Proof. by rewrite predeqE => ?; split=> [[? []]|[[]]]. Qed.
 

theories/topology.v

@@ -196,6 +196,8 @@ Require Import boolp reals classical_sets posnum.
 (*                                     cover-based definition of compactness. *)
 (*                     connected A <-> the only non empty subset of A which   *)
 (*                                     is both open and closed in A is A.     *)
+(*                    kolmogorov T <-> T is a Kolmogorov space (T_0).         *)
+(*                    accessible T <-> T is an accessible space (T_1).        *)
 (*                    separated A B == the two sets A and B are separated     *)
 (*                      component x == the connected component of point x     *)
 (*                      [locally P] := forall a, A a -> G (within A (nbhs x)) *)
@@ -2829,33 +2831,31 @@ End Covers.
 
 Section separated_topologicalType.
 Variable (T : topologicalType).
+Implicit Types x y : T.
 
 Local Open Scope classical_set_scope.
 
-Definition T_0 : Prop := forall (x y : T), x != y -> exists p, (p \in (nbhs x) /\ y \in (~` p)) \/ (p \in (nbhs y) /\ x \in (~` p)).
+Definition kolmogorov := forall x y, x != y ->
+  exists A : set T, (A \in nbhs x /\ y \in ~` A) \/ (A \in nbhs y /\ x \in ~` A).
 
-Definition T_1 : Prop := forall (x y : T), x != y -> exists p, (open p /\ x \in p /\ y \in (~` p)).
+Definition accessible := forall x y, x != y ->
+  exists A : set T, open A /\ x \in A /\ y \in ~` A.
 
-Lemma T_1_singleton_closed : T_1 -> forall x:T, closed [set x].
+Lemma accessible_closed_set1 : accessible -> forall x, closed [set x].
 Proof.
-  move => T1 x; rewrite -[set1 _]setCK; apply: closedC.
-  rewrite openE -set1CE /interior => y //= /eqP xNeqY.
-  rewrite nbhsE => //=.
-  have := T1 _ _ xNeqY => -[] U [] ? [] ? ?.
-  exists U ; split.
-    by rewrite /open_nbhs ; split; by [|rewrite -in_setE].
-  by apply: setC_subset_set1C.
+move=> T1 x; rewrite -[X in closed X]setCK; apply: closedC.
+rewrite openE setC1E => y /eqP /T1 [U [oU [yU xU]]].
+rewrite /interior nbhsE /=; exists U; split; last exact: mem_setC_subset.
+by split => //; rewrite -in_setE.
 Qed.
 
-Definition T_1entailsT_0 : T_1 -> T_0.
+Definition accessible_kolmogorov : accessible -> kolmogorov.
 Proof.
-  rewrite /T_0 => T_1 x ? xneqy.
-  have:= (T_1 _ _ xneqy) => -[] p [] ? [] /asboolP ? ?.
-  have: open_nbhs x p by split; by [].
-  rewrite open_nbhsE => -[] ? H; exists p; left; split ; by [apply/asboolP|].
+move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split => //.
+by rewrite nbhsE inE /=; exists A; split => //; split => //; rewrite -in_setE.
 Qed.
 
-Definition close (x y : T) : Prop := forall M, open_nbhs y M -> closure M x.
+Definition close x y : Prop := forall M, open_nbhs y M -> closure M x.
 
 Lemma closeEnbhs x : close x = cluster (nbhs x).
 Proof.
@@ -2871,16 +2871,15 @@ Proof.
 by rewrite closeEnbhs; under eq_fun do rewrite -meets_openl -meets_openr.
 Qed.
 
-Lemma close_sym (x y : T) : close x y -> close y x.
+Lemma close_sym x y : close x y -> close y x.
 Proof. by rewrite !closeEnbhs /cluster/= meetsC. Qed.
 
-Lemma cvg_close {F} {FF : ProperFilter F} (x y : T) :
-  F --> x -> F --> y -> close x y.
+Lemma cvg_close {F} {FF : ProperFilter F} x y : F --> x -> F --> y -> close x y.
 Proof.
 by move=> /sub_meets sx /sx; rewrite closeEnbhs; apply; apply/proper_meetsxx.
 Qed.
 
-Lemma close_refl (x : T) : close x x.
+Lemma close_refl x : close x x.
 Proof. exact: (@cvg_close (nbhs x)). Qed.
 Hint Resolve close_refl : core.
 
@@ -2894,7 +2893,7 @@ have [/(cvg_trans F12)/cvgP//|dvgF2] := pselect (cvg F2).
 rewrite dvgP // dvgP //; exact/close_refl.
 Qed.
 
-Lemma cvgx_close (x y : T) : x --> y -> close x y.
+Lemma cvgx_close x y : x --> y -> close x y.
 Proof. exact: cvg_close. Qed.
 
 Lemma cvgi_close T' {F} {FF : ProperFilter F} (f : T' -> set T) (l l' : T) :
@@ -2909,13 +2908,13 @@ Grab Existential Variables. all: end_near. Qed.
 Definition cvg_toi_locally_close := @cvgi_close.
 
 Lemma open_hausdorff : hausdorff T =
-  (forall x y : T, x != y ->
+  forall x y, x != y ->
     exists2 AB, (x \in AB.1 /\ y \in AB.2) &
-                [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0]).
+                [/\ open AB.1, open AB.2 & AB.1 `&` AB.2 == set0].
 Proof.
 rewrite propeqE; split => [T_filterT2|T_openT2] x y.
-  have := contra_not _ _ (T_filterT2 x y); rewrite (rwP eqP) (rwP negP) => cl /cl.
-  rewrite [cluster _ _](rwP forallp_asboolP) => /negP.
+  have := contra_not _ _ (T_filterT2 x y); rewrite (rwP eqP) (rwP negP).
+  move=> /[apply]; rewrite [cluster _ _](rwP forallp_asboolP) => /negP.
   rewrite forallbE => /existsp_asboolPn/=[A]/negP/existsp_asboolPn/=[B].
   rewrite [nbhs _ _ -> _](rwP imply_asboolP) => /negP.
   rewrite asbool_imply !negb_imply => /andP[/asboolP xA] /andP[/asboolP yB].
@@ -2931,22 +2930,22 @@ Qed.
 
 Hypothesis sep : hausdorff T.
 
-Lemma closeE (x y : T) : close x y = (x = y).
+Lemma closeE x y : close x y = (x = y).
 Proof.
 rewrite propeqE; split; last by move=> ->; exact: close_refl.
 by rewrite closeEnbhs; exact: sep.
 Qed.
 
-Lemma close_eq (y x : T) : close x y -> x = y.
+Lemma close_eq x y : close x y -> x = y.
 Proof. by rewrite closeE. Qed.
 
 Lemma cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : T | F --> x].
 Proof. move=> Fx Fy; rewrite -closeE //; exact: (@cvg_close F). Qed.
 
-Lemma cvg_eq (x y : T) : x --> y -> x = y.
+Lemma cvg_eq x y : x --> y -> x = y.
 Proof. by rewrite -closeE //; apply: cvg_close. Qed.
 
-Lemma lim_id (x : T) : lim x = x.
+Lemma lim_id x : lim x = x.
 Proof. by apply/esym/cvg_eq/cvg_ex; exists x. Qed.
 
 Lemma cvg_lim {F} {FF : ProperFilter F} (l : T) : F --> l -> lim F = l.