Merge pull request #471 from math-comp/fixes_461

fixes #461
math-comp · Nov 8, 2021 · 780df29 · 780df29
2 parents edf190c + 6b8424d
commit 780df29
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -356,6 +356,8 @@
   + lemma `continuous_cst`
 - in `csum.v`:
   + lemma `ub_ereal_sup_adherent_img`
+- in `topology.v`:
+  + definition `cvg_to_locally`
 
 ### Infrastructure
 

diff --git a/theories/topology.v b/theories/topology.v
@@ -3910,8 +3910,6 @@ Lemma cvg_ballP {F} {FF : Filter F} (y : M) :
   F --> y <-> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'.
 Proof. by rewrite -filter_fromP !nbhs_simpl /=. Qed.
 
-Definition cvg_to_locally := @cvg_ballP.
-
 Lemma cvg_ballPpos {F} {FF : Filter F} (y : M) :
   F --> y <-> forall eps : {posnum R}, \forall y' \near F, ball y eps%:num y'.
 Proof.