fix

- removed useless `setC1E` (it is convertible and `inE` yields the same result)
- removed `mem_setC_subset` which was a duplicate of `setC_subset_set1C`
- generalized and renamed the latter to `subsetC1`
- removed all uses of `-in_setE`

CHANGELOG_UNRELEASED.md

@@ -8,12 +8,14 @@
   + lemma `setDIr`
   + lemmas `setMT`, `setTM`, `setMI`
   + lemmas `setSM`, `setM_bigcupr`, `setM_bigcupl`
-  + lemmas `setC1E`, `mem_setC_subset`
 - in `topology.v`:
   + definitions `kolmogorov`, `accessible`
   + lemmas `accessible_closed_set1`, `accessible_kolmogorov`
 
 ### Changed
+- in `topology.v`:
+  + renamed and generalized `setC_subset_set1C` implication to
+    equivalence `subsetC1`
 
 - in `normedtype.v`:
   + `nbhs_minfty_lt` renamed to `nbhs_ninfty_lt_pos` and changed to not use `{posnum R}`

theories/classical_sets.v

@@ -44,7 +44,7 @@ Require Import boolp.
 (*                        A.`2 == set of points a such that there exists b so *)
 (*                                that A (b, a).                              *)
 (*                        ~` A == complement of A.                            *)
-(*                   [set ~ a] == complement of [set a].                      *)
+(*                    [set~ a] == complement of [set a].                      *)
 (*                     A `\` B == complement of B in A.                       *)
 (*                      A `\ a == A deprived of a.                            *)
 (*          \bigcup_(i in P) F == union of the elements of the family F whose *)
@@ -492,10 +492,11 @@ Proof. by rewrite subsets_disjoint setCK. Qed.
 
 Lemma setCT : ~` setT = set0 :> set T. Proof. by rewrite -setC0 setCK. 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 subsetC1 x A : (A `<=` [set~ x]) = (x \in ~` A).
+Proof.
+rewrite !inE; apply/propext; split; first by move/[apply]; apply.
+by move=> NAx y; apply: contraPnot => ->.
+Qed.
 
 Lemma setDE A B : A `\` B = A `&` ~` B. Proof. by []. Qed.
 
@@ -600,14 +601,6 @@ Qed.
 Lemma nonsubset A B : ~ (A `<=` B) -> A `&` ~` B !=set0.
 Proof. by rewrite -setD_eq0 setDE -set0P => /eqP. 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 setU_eq0 A B : (A `|` B = set0) = ((A = set0) /\ (B = set0)).
 Proof. by rewrite -!subset0 subUset. Qed.
 

theories/topology.v

@@ -2924,15 +2924,15 @@ Definition accessible := forall x y, x != y ->
 Lemma accessible_closed_set1 : accessible -> forall x, closed [set x].
 Proof.
 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.
+rewrite openE => y /eqP /T1 [U [oU [yU xU]]].
+rewrite /interior nbhsE /=; exists U; split; last by rewrite subsetC1.
+by split=> //; rewrite inE in yU.
 Qed.
 
 Definition accessible_kolmogorov : accessible -> kolmogorov.
 Proof.
-move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split => //.
-by rewrite nbhsE inE /=; exists A; split => //; split => //; rewrite -in_setE.
+move=> T1 x y /T1 [A [oA [xA yA]]]; exists A; left; split=> //.
+by rewrite nbhsE inE; exists A; do !split=> //; rewrite inE in xA.
 Qed.
 
 Definition close x y : Prop := forall M, open_nbhs y M -> closure M x.