diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 531fe28a7e..9fee1fd696 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -153,6 +153,9 @@
 - in `Rstruct.v`:
   + lemma `RsqrtE`
 
+- in `normedtype.v`:
+  + `cvg_at_right_filter`, `cvg_at_left_filter`
+
 ### Deprecated
 
 ### Removed
diff --git a/theories/normedtype.v b/theories/normedtype.v
index 4ec2cd6271..686872e076 100644
--- a/theories/normedtype.v
+++ b/theories/normedtype.v
@@ -1514,10 +1514,12 @@ End open_itv_subset.
 Section at_left_right_topologicalType.
 Variables (R : numFieldType) (V : topologicalType) (f : R -> V) (x : R).
 
-Lemma cvg_at_right_filter : f z @[z --> x] --> f x -> f z @[z --> x^'+] --> f x.
+Lemma cvg_at_right_filter (l : V) :
+  f z @[z --> x] --> l -> f z @[z --> x^'+] --> l.
 Proof. exact: (@cvg_within_filter _ _ _ (nbhs x)). Qed.
 
-Lemma cvg_at_left_filter : f z @[z --> x] --> f x -> f z @[z --> x^'-] --> f x.
+Lemma cvg_at_left_filter (l : V) :
+  f z @[z --> x] --> l -> f z @[z --> x^'-] --> l.
 Proof. exact: (@cvg_within_filter _ _ _ (nbhs x)). Qed.
 
 Lemma cvg_at_right_within : f x @[x --> x^'+] --> f x ->
@@ -2494,7 +2496,7 @@ End prod_NormedModule.
 Section example_of_sharing.
 Variables (K : numDomainType).
 
-Example matrix_triangke m n (M N : 'M[K]_(m.+1, n.+1)) :
+Example matrix_triangle m n (M N : 'M[K]_(m.+1, n.+1)) :
   `|M + N| <= `|M| + `|N|.
 Proof. exact: ler_normD. Qed.
 
diff --git a/theories/topology_theory/topology_structure.v b/theories/topology_theory/topology_structure.v
index 5bbcd306c6..1b6b57aae1 100644
--- a/theories/topology_theory/topology_structure.v
+++ b/theories/topology_theory/topology_structure.v
@@ -919,7 +919,6 @@ Proof. by rewrite -interiorC interiorEbigcup. Qed.
 #[deprecated(since="mathcomp-analysis 1.7.0", note="use `interiorC` and `interiorEbigcup` instead")]
 Notation closureC := closureC_deprecated (only parsing).
 
-
 Definition dense (T : topologicalType) (S : set T) :=
   forall (O : set T), O !=set0 -> open O -> O `&` S !=set0.