renaming

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -73,7 +73,7 @@
   + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`
 
 - in `topology_structure.v`:
-  + lemma `limit_pointNE`
+  + lemma `not_limit_pointE`
 
 - in `separation_axioms.v`:
   + lemmas `limit_point_closed`

theories/topology_theory/separation_axioms.v

@@ -205,11 +205,11 @@ Lemma limit_point_closed {T : topologicalType} (A : set T) :
   accessible_space T -> closed (limit_point A).
 Proof.
 move=> accT; rewrite -openC openE/= => a.
-rewrite /setC/= limit_pointNE => -[X].
+rewrite /setC/= not_limit_pointE => -[X].
 rewrite nbhsE/= => -[U oaU UX] XAa.
 rewrite /interior nbhsE/=.
 exists U => // x Ux /=.
-rewrite limit_pointNE.
+rewrite not_limit_pointE.
 have [xa|xneqa] := eqVneq x a.
   exists U; rewrite xa; first exact: open_nbhs_nbhs.
   by apply: subset_trans XAa; exact: setIS.

theories/topology_theory/topology_structure.v

@@ -689,7 +689,7 @@ Proof. by rewrite limit_pointEnbhs; under eq_fun do rewrite meets_openr. Qed.
 Lemma subset_limit_point E : limit_point E `<=` closure E.
 Proof. by move=> t Et U tU; have [p [? ? ?]] := Et _ tU; exists p. Qed.
 
-Lemma limit_pointNE A a : (~ limit_point A a) =
+Lemma not_limit_pointE A a : (~ limit_point A a) =
   exists2 X : set T, nbhs a X & A `&` X `<=` [set a].
 Proof.
 rewrite /limit_point/= -existsNE exists2E; apply: eq_exists => X/=.