Merge pull request #381 from math-comp/coord_continuous

minor generalization
math-comp · Jun 1, 2021 · 09e03a7 · 09e03a7
2 parents 9ece6a1 + c6cc36f
commit 09e03a7
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -103,6 +103,8 @@
 - in `ereal.v`:
   + argument of `%:E` in `%R` by default
   + `F` argument of `\sum` in `%E` by default
+- in `normedtype.v`:
+  + `coord_continuous` generalized
 
 ### Renamed
 

diff --git a/theories/normedtype.v b/theories/normedtype.v
@@ -356,13 +356,12 @@ by split=> zxy e /zxy; rewrite [z + _]addrC [_ + x]addrC.
 Qed.
 
 Lemma coord_continuous {K : numFieldType} m n i j :
-  continuous (fun M : 'M[K]_(m.+1, n.+1) => M i j).
+  continuous (fun M : 'M[K]_(m, n) => M i j).
 Proof.
 move=> /= M s /= /(nbhs_ballP (M i j)) [e e0 es].
 apply/nbhs_ballP; exists e => //= N MN; exact/es/MN.
 Qed.
 
-
 Global Instance Proper_nbhs'_numFieldType (R : numFieldType) (x : R) :
   ProperFilter (nbhs' x).
 Proof.