typos

theories/topology_theory/pseudometric_structure.v

@@ -9,7 +9,7 @@ From mathcomp Require Import uniform_structure.
 (* # PseudoMetric Spaces                                                      *)
 (* This file provides pseudometric spaces, complete pseudometric spaces,      *)
 (* and the corresponding theory. Note that a classic metric space is simply   *)
-(* pseudometric + hausdorff. However we will make extensive use of the of the *)
+(* pseudometric + hausdorff. However we will make extensive use of the        *)
 (* non-hausdorff case, such as in our proof of Urysohn's lemma.               *)
 (*                                                                            *)
 (* ## Mathematical structures                                                 *)

theories/topology_theory/separation_axioms.v

@@ -15,7 +15,7 @@ From mathcomp Require Import connected supremum_topology sigT_topology.
 (* # Separation Axioms                                                        *)
 (*                                                                            *)
 (* This file introduces the separation axioms, a series of topological        *)
-(* properties about separating points and sets. They are somtimes denoted by  *)
+(* properties about separating points and sets. They are sometimes denoted by *)
 (* the names T0 through T6. Although we use their full names (hausdorff,      *)
 (* accessible, uniform, etc). This file also provides related topological     *)
 (* properties like zero dimensional and perfect, and discrete.                *)