From 5caecf234a421020edb43158a092f792f187ab65 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 24 Apr 2025 17:19:19 +0900 Subject: [PATCH] typos --- theories/topology_theory/pseudometric_structure.v | 2 +- theories/topology_theory/separation_axioms.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/topology_theory/pseudometric_structure.v b/theories/topology_theory/pseudometric_structure.v index acbe4b4cc2..477bb5a3ed 100644 --- a/theories/topology_theory/pseudometric_structure.v +++ b/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 *) diff --git a/theories/topology_theory/separation_axioms.v b/theories/topology_theory/separation_axioms.v index 24893b3033..bbacd47f90 100644 --- a/theories/topology_theory/separation_axioms.v +++ b/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. *)