doc(Topology): fix typos (#32659)

Typos found and fixed by Codex.

Author: harahu

Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean

@@ -12,7 +12,7 @@ public import Mathlib.Order.Filter.AtTopBot.Finset
 /-!
 # Infinite sum and products that converge uniformly
 
-# Main definitions
+## Main definitions
 - `HasProdUniformlyOn f g s` : `∏ i, f i b` converges uniformly on `s` to `g`.
 - `HasProdLocallyUniformlyOn f g s` : `∏ i, f i b` converges locally uniformly on `s` to `g`.
 - `HasProdUniformly f g` : `∏ i, f i b` converges uniformly to `g`.

Mathlib/Topology/Bases.lean

@@ -45,7 +45,7 @@ conditions are equivalent in this case).
   the space.
 
 ## Implementation Notes
-For our applications we are interested that there exists a countable basis, but we do not need the
+For our applications we are interested in the existence of a countable basis, but we do not need the
 concrete basis itself. This allows us to declare these type classes as `Prop` to use them as mixins.
 
 ## TODO

Mathlib/Topology/EMetricSpace/PairReduction.lean

@@ -57,9 +57,9 @@ natural number `k` greater than zero such that `|{x ∈ V | d(t, x) ≤ kc}| ≤
 We construct a sequence `Vᵢ` of subsets of `J`, a sequence `tᵢ ∈ Vᵢ` and a sequence of `rᵢ : ℕ`
 inductively as follows (see `logSizeBallSeq`):
 
-* `V₀ = J`, `tₒ` is chosen arbitrarily in `J`, `r₀` is the log-size radius of `t₀` in `V₀`
-* `Vᵢ₊ᵢ = Vᵢ \ Bᵢ` where `Bᵢ := {x ∈ V | d(t, x) ≤ (rᵢ - 1) c}`, `tᵢ₊₁` is chosen arbitrarily in
-  `Vᵢ₊₁` (if it is nonempty), `rᵢ₊₁` is the log-size radius of `tᵢ₊₁` in `Vᵢ₊ᵢ`.
+* `V₀ = J`, `t₀` is chosen arbitrarily in `J`, `r₀` is the log-size radius of `t₀` in `V₀`
+* `Vᵢ₊₁ = Vᵢ \ Bᵢ` where `Bᵢ := {x ∈ V | d(t, x) ≤ (rᵢ - 1) c}`, `tᵢ₊₁` is chosen arbitrarily in
+  `Vᵢ₊₁` (if it is nonempty), `rᵢ₊₁` is the log-size radius of `tᵢ₊₁` in `Vᵢ₊₁`.
 
 Then `Vᵢ` is a strictly decreasing sequence (see `card_finset_logSizeBallSeq_add_one_lt`) until
 `Vᵢ` is empty. In particular `Vᵢ = ∅` for `i ≥ |J|`
@@ -176,9 +176,9 @@ def logSizeBallStruct.ball (struct : logSizeBallStruct T) (c : ℝ≥0∞) :
 variable [DecidableEq T]
 
 /-- We recursively define a log-size ball sequence `(Vᵢ, tᵢ, rᵢ)` by
-  * `V₀ = J`, `tₒ` is chosen arbitrarily in `J`, `r₀` is the log-size radius of `t₀` in `V₀`
-  * `Vᵢ₊ᵢ = Vᵢ \ {x ∈ V | d(t, x) ≤ (rᵢ - 1)c}`, `tᵢ₊₁` is chosen arbitrarily in `Vᵢ₊₁, rᵢ₊₁` is
-    the log-size radius of `tᵢ₊₁` in `Vᵢ₊ᵢ`. -/
+  * `V₀ = J`, `t₀` is chosen arbitrarily in `J`, `r₀` is the log-size radius of `t₀` in `V₀`
+  * `Vᵢ₊₁ = Vᵢ \ {x ∈ V | d(t, x) ≤ (rᵢ - 1)c}`, `tᵢ₊₁` is chosen arbitrarily in `Vᵢ₊₁`, `rᵢ₊₁` is
+    the log-size radius of `tᵢ₊₁` in `Vᵢ₊₁`. -/
 noncomputable
 def logSizeBallSeq (J : Finset T) (hJ : J.Nonempty) (a c : ℝ≥0∞) : ℕ → logSizeBallStruct T
   | 0 => {finset := J, point := hJ.choose, radius := logSizeRadius hJ.choose J a c}

Mathlib/Topology/Homotopy/HSpaces.lean

@@ -14,16 +14,16 @@ public import Mathlib.Topology.Path
 
 This file defines H-spaces mainly following the approach proposed by Serre in his paper
 *Homologie singulière des espaces fibrés*. The idea beneath `H-spaces` is that they are topological
-spaces with a binary operation `⋀ : X → X → X` that is a homotopic-theoretic weakening of an
-operation what would make `X` into a topological monoid.
-In particular, there exists a "neutral element" `e : X` such that `fun x ↦e ⋀ x` and
+spaces with a binary operation `⋀ : X → X → X` that is a homotopy-theoretic weakening of an
+operation that would make `X` into a topological monoid.
+In particular, there exists a "neutral element" `e : X` such that `fun x ↦ e ⋀ x` and
 `fun x ↦ x ⋀ e` are homotopic to the identity on `X`, see
 [the Wikipedia page of H-spaces](https://en.wikipedia.org/wiki/H-space).
 
 Some notable properties of `H-spaces` are
 * Their fundamental group is always abelian (by the same argument for topological groups);
 * Their cohomology ring comes equipped with a structure of a Hopf-algebra;
-* The loop space based at every `x : X` carries a structure of an `H-spaces`.
+* The loop space based at every `x : X` carries a structure of an `H-space`.
 
 ## Main Results
 
@@ -32,14 +32,14 @@ Some notable properties of `H-spaces` are
 * Given two `H-spaces` `X` and `Y`, their product is again an `H`-space. We show in an example that
   starting with two topological groups `G, G'`, the `H`-space structure on `G × G'` is
   definitionally equal to the product of `H-space` structures on `G` and `G'`.
-* The loop space based at every `x : X` carries a structure of an `H-spaces`.
+* The loop space based at every `x : X` carries a structure of an `H-space`.
 
 ## To Do
 * Prove that for every `NormedAddTorsor Z` and every `z : Z`, the operation
   `fun x y ↦ midpoint x y` defines an `H-space` structure with `z` as a "neutral element".
 * Prove that `S^0`, `S^1`, `S^3` and `S^7` are the unique spheres that are `H-spaces`, where the
   first three inherit the structure because they are topological groups (they are Lie groups,
-  actually), isomorphic to the invertible elements in `ℤ`, in `ℂ` and in the quaternion; and the
+  actually), isomorphic to the invertible elements in `ℤ`, in `ℂ` and in the quaternions; and the
   fourth from the fact that `S^7` coincides with the octonions of norm 1 (it is not a group, in
   particular, only has an instance of `MulOneClass`).
 

Mathlib/Topology/MetricSpace/Bounded.lean

@@ -336,7 +336,7 @@ theorem isBounded_Ioc (a b : α) : IsBounded (Ioc a b) :=
 theorem isBounded_Ioo (a b : α) : IsBounded (Ioo a b) :=
   (totallyBounded_Ioo a b).isBounded
 
-/-- In a pseudo metric space with a conditionally complete linear order such that the order and the
+/-- In a pseudometric space with a conditionally complete linear order such that the order and the
 metric structure give the same topology, any order-bounded set is metric-bounded. -/
 theorem isBounded_of_bddAbove_of_bddBelow {s : Set α} (h₁ : BddAbove s) (h₂ : BddBelow s) :
     IsBounded s :=

Mathlib/Topology/MetricSpace/Gluing.lean

@@ -450,7 +450,7 @@ variable {X : Type u} {Y : Type v} {Z : Type w}
 variable [Nonempty Z] [MetricSpace Z] [MetricSpace X] [MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y}
   {ε : ℝ}
 
-/-- Given two isometric embeddings `Φ : Z → X` and `Ψ : Z → Y`, we define a pseudo metric space
+/-- Given two isometric embeddings `Φ : Z → X` and `Ψ : Z → Y`, we define a pseudometric space
 structure on `X ⊕ Y` by declaring that `Φ x` and `Ψ x` are at distance `0`. -/
 def gluePremetric (hΦ : Isometry Φ) (hΨ : Isometry Ψ) : PseudoMetricSpace (X ⊕ Y) where
   dist := glueDist Φ Ψ 0

Mathlib/Topology/MetricSpace/PiNat.lean

@@ -810,7 +810,7 @@ attribute [scoped instance] PiCountable.edist
 section PseudoEMetricSpace
 variable [∀ i, PseudoEMetricSpace (F i)]
 
-/-- Given a countable family of extended pseudo metric spaces,
+/-- Given a countable family of extended pseudometric spaces,
 one may put an extended distance on their product `Π i, E i`.
 
 It is highly non-canonical, though, and therefore not registered as a global instance.

Mathlib/Topology/MetricSpace/ProperSpace.lean

@@ -60,7 +60,7 @@ instance Metric.sphere.compactSpace {α : Type*} [PseudoMetricSpace α] [ProperS
 variable [PseudoMetricSpace α]
 
 -- see Note [lower instance priority]
-/-- A proper pseudo metric space is sigma compact, and therefore second countable. -/
+/-- A proper pseudometric space is sigma compact, and therefore second countable. -/
 instance (priority := 100) secondCountable_of_proper [ProperSpace α] :
     SecondCountableTopology α := by
   -- We already have `sigmaCompactSpace_of_locallyCompact_secondCountable`, so we don't

Mathlib/Topology/MetricSpace/Pseudo/Defs.lean

@@ -133,7 +133,7 @@ class PseudoMetricSpace (α : Type u) : Type u extends Dist α where
   cobounded_sets : (Bornology.cobounded α).sets =
     { s | ∃ C : ℝ, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C } := by intros; rfl
 
-/-- Two pseudo metric space structures with the same distance function coincide. -/
+/-- Two pseudometric space structures with the same distance function coincide. -/
 @[ext]
 theorem PseudoMetricSpace.ext {α : Type*} {m m' : PseudoMetricSpace α}
     (h : m.toDist = m'.toDist) : m = m' := by
@@ -990,7 +990,7 @@ example {α} [U : UniformSpace α] (m : PseudoMetricSpace α)
     (PseudoMetricSpace.replaceUniformity m H).toBornology = m.toBornology := by
   with_reducible_and_instances rfl
 
-/-- Build a new pseudo metric space from an old one where the bundled topological structure is
+/-- Build a new pseudometric space from an old one where the bundled topological structure is
 provably (but typically non-definitionaly) equal to some given topological structure.
 See Note [forgetful inheritance].
 See Note [reducible non-instances].

Mathlib/Topology/Metrizable/Basic.lean

@@ -29,7 +29,7 @@ namespace TopologicalSpace
 variable {ι X Y : Type*} {A : ι → Type*} [TopologicalSpace X] [TopologicalSpace Y] [Finite ι]
   [∀ i, TopologicalSpace (A i)]
 
-/-- A topological space is *pseudo metrizable* if there exists a pseudo metric space structure
+/-- A topological space is *pseudometrizable* if there exists a pseudometric space structure
 compatible with the topology. To minimize imports, we implement this class in terms of the
 existence of a countably generated unifomity inducing the topology, which is mathematically
 equivalent.
@@ -41,7 +41,7 @@ class PseudoMetrizableSpace (X : Type*) [t : TopologicalSpace X] : Prop where
   exists_countably_generated :
     ∃ u : UniformSpace X, u.toTopologicalSpace = t ∧ (uniformity X).IsCountablyGenerated
 
-/-- A uniform space with countably generated `𝓤 X` is pseudo metrizable. -/
+/-- A uniform space with countably generated `𝓤 X` is pseudometrizable. -/
 instance (priority := 100) _root_.UniformSpace.pseudoMetrizableSpace {X : Type*}
     [u : UniformSpace X] [hu : IsCountablyGenerated (uniformity X)] : PseudoMetrizableSpace X :=
   ⟨⟨u, rfl, hu⟩⟩
@@ -75,8 +75,8 @@ instance pseudoMetrizableSpace_prod [PseudoMetrizableSpace X] [PseudoMetrizableS
     pseudoMetrizableSpaceUniformity_countably_generated Y
   inferInstance
 
-/-- Given an inducing map of a topological space into a pseudo metrizable space, the source space
-is also pseudo metrizable. -/
+/-- Given an inducing map of a topological space into a pseudometrizable space, the source space
+is also pseudometrizable. -/
 theorem _root_.Topology.IsInducing.pseudoMetrizableSpace [PseudoMetrizableSpace Y] {f : X → Y}
     (hf : IsInducing f) : PseudoMetrizableSpace X :=
   let u : UniformSpace Y := pseudoMetrizableSpaceUniformity Y