fixing typos

CHANGELOG_UNRELEASED.md

@@ -40,7 +40,7 @@
   + lemmas `sup_ent_filter`, `sup_ent_refl`, `sup_ent_inv`, `sup_ent_split`,
     `sup_ent_nbhs` are now `Local`
 
-- Th function `map_pair` was moved from `topology.v` to `mathcomp_extras.v`.
+- The function `map_pair` was moved from `topology.v` to `mathcomp_extra.v`.
 
 ### Renamed
 

theories/function_spaces.v

@@ -13,24 +13,24 @@ Require Import reals signed topology separation_axioms.
 (*                                                                            *)
 (* ## Topologies on `U -> V`                                                  *)
 (* There is no canonical topology on `U->V` in this library. Mathematically,  *)
-(* the right topology usually depends on context. We provide 3 general        *)
+(* the right topology usually depends on context. We provide three general    *)
 (* options in this file which work for various amounts of structures on the   *)
 (* domain and codomain.                                                       *)
 (*                                                                            *)
 (* Topologies we consider are:                                                *)
 (* - Topology of pointwise convergence                                        *)
-(*   - requires only a topology on V                                          *)
+(*   + requires only a topology on V                                          *)
 (* - Topology of uniform convergence                                          *)
-(*   - requires only a uniformity on V                                        *)
+(*   + requires only a uniformity on V                                        *)
 (* - Topology of uniform convergence on subspaces                             *)
-(*   - requires only a uniformity on V                                        *)
+(*   + requires only a uniformity on V                                        *)
 (* - The compact-open topology                                                *)
-(*   - requires a topology on U and V                                         *)
+(*   + requires a topology on U and V                                         *)
 (*                                                                            *)
 (* if you're looking for the topology of compact convergence, note that       *)
 (* it is exactly the compact-open topology via `compact_open_fam_compactP`.   *)
 (*                                                                            *)
-(* To locally asign a topology to `->`, import one of the following modules   *)
+(* To locally assign a topology to `->`, import one of the following modules  *)
 (* - ArrowAsProduct assigns the product topology                              *)
 (* - ArrowAsUniformType assigns the uniform topology                          *)
 (* - ArrowAsCompactOpen assign the compact-open topology                      *)

theories/topology_theory/matrix_topology.v

@@ -6,8 +6,8 @@ Require Import signed topology_structure uniform_structure pseudometric_structur
 (**md**************************************************************************)
 (* # Matrix topology                                                          *)
 (* ```                                                                        *)
-(*                  mx_ent m n A == entourages for the m x n matricies        *)
-(*                 mx_ball m n A == balls for the m x n matricies             *)
+(*                  mx_ent m n A == entourages for the m x n matrices        *)
+(*                 mx_ball m n A == balls for the m x n matrices             *)
 (* ```                                                                        *)
 (* Matrices `'M[T]_(m, n)` are endowed with the structures of:                *)
 (* - topology                                                                 *)