diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 0bf2951ee..62dfcae47 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -72,6 +72,12 @@
 - in `derive.v`:
   + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV`
 
+- in `topology_structure.v`:
+  + lemma `limit_pointNE`
+
+- in `separation_axioms.v`:
+  + lemmas `limit_point_closed`
+
 ### Changed
 
 - in `constructive_ereal.v`: fixed the infamous `%E` scope bug.
diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v
index 9061ed845..7ea0e97a4 100644
--- a/theories/topology_theory/separation_axioms.v
+++ b/theories/topology_theory/separation_axioms.v
@@ -201,6 +201,31 @@ Arguments hausdorff_space : clear implicits.
 Arguments accessible_space : clear implicits.
 Arguments kolmogorov_space : clear implicits.
 
+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 nbhsE/= => -[U oaU UX] XAa.
+rewrite /interior nbhsE/=.
+exists U => // x Ux /=.
+rewrite limit_pointNE.
+have [xa|xneqa] := eqVneq x a.
+  exists U; rewrite xa; first exact: open_nbhs_nbhs.
+  by apply: subset_trans XAa; exact: setIS.
+exists (U `&` [set~ a]).
+  apply: open_nbhs_nbhs; split.
+    apply: openI; first by case: oaU.
+    by rewrite openC; exact: accessible_closed_set1.
+  by split => //; exact/eqP.
+apply: (@subset_trans _ (A `&` (X `&` [set~ a]))).
+  by apply: setIS; exact: setSI.
+apply: (@subset_trans _ ([set a] `&` [set~ a])).
+  by rewrite setIA; exact: setSI.
+by rewrite setICr.
+Qed.
+Arguments limit_point_closed {T} A.
+
 Lemma subspace_hausdorff {T : topologicalType} (A : set T) :
   hausdorff_space T -> hausdorff_space (subspace A).
 Proof.
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index ac7222837..ac8b72c07 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -689,6 +689,15 @@ 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) =
+  exists2 X : set T, nbhs a X & A `&` X `<=` [set a].
+Proof.
+rewrite /limit_point/= -existsNE exists2E; apply: eq_exists => X/=.
+rewrite not_implyE -forallNE; congr and; apply: eq_forall => t/=.
+rewrite and3E not_andE (propext (rwP negP)) negbK implyE orC.
+by rewrite -(propext (rwP eqP)).
+Qed.
+
 Definition isolated (A : set T) (x : T) :=
   x \in A /\ exists2 V, nbhs x V & V `&` A = [set x].