[Merged by Bors] - doc(Topology): fix typos

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

Mathlib/Topology/Metrizable/Uniformity.lean

@@ -20,7 +20,7 @@ The proof follows [Sergey Melikhov, Metrizable uniform spaces][melikhov2011].
 ## Main definitions
 
 * `PseudoMetricSpace.ofPreNNDist`: given a function `d : X → X → ℝ≥0` such that `d x x = 0` and
-  `d x y = d y x` for all `x y : X`, constructs the maximal pseudo metric space structure such that
+  `d x y = d y x` for all `x y : X`, constructs the maximal pseudometric space structure such that
   `NNDist x y ≤ d x y` for all `x y : X`.
 
 * `UniformSpace.pseudoMetricSpace`: given a uniform space `X` with countably generated `𝓤 X`,
@@ -35,8 +35,8 @@ The proof follows [Sergey Melikhov, Metrizable uniform spaces][melikhov2011].
   then there exists a `PseudoMetricSpace` structure that is compatible with this `UniformSpace`
   structure. Use `UniformSpace.pseudoMetricSpace` or `UniformSpace.metricSpace` instead.
 
-* `UniformSpace.pseudoMetrizableSpace`: a uniform space with countably generated `𝓤 X` is pseudo
-  metrizable.
+* `UniformSpace.pseudoMetrizableSpace`: a uniform space with countably generated `𝓤 X` is
+  pseudometrizable.
 
 * `UniformSpace.metrizableSpace`: a T₀ uniform space with countably generated `𝓤 X` is
   metrizable. This is not an instance to avoid loops.
@@ -56,7 +56,7 @@ variable {X : Type*}
 
 namespace PseudoMetricSpace
 
-/-- The maximal pseudo metric space structure on `X` such that `dist x y ≤ d x y` for all `x y`,
+/-- The maximal pseudometric space structure on `X` such that `dist x y ≤ d x y` for all `x y`,
 where `d : X → X → ℝ≥0` is a function such that `d x x = 0` and `d x y = d y x` for all `x`, `y`. -/
 noncomputable def ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x, d x x = 0)
     (dist_comm : ∀ x y, d x y = d y x) : PseudoMetricSpace X where
@@ -186,10 +186,10 @@ protected theorem UniformSpace.metrizable_uniformity (X : Type*) [UniformSpace X
     Define `d x y : ℝ≥0` to be `(1 / 2) ^ n`, where `n` is the minimal index of `U n` that
     separates `x` and `y`: `(x, y) ∉ U n`, or `0` if `x` is not separated from `y`. This function
     satisfies the assumptions of `PseudoMetricSpace.ofPreNNDist` and
-    `PseudoMetricSpace.le_two_mul_dist_ofPreNNDist`, hence the distance given by the former pseudo
-    metric space structure is Lipschitz equivalent to the `d`. Thus the uniformities generated by
-    `d` and `dist` are equal. Since the former uniformity is equal to `𝓤 X`, the latter is equal to
-    `𝓤 X` as well. -/
+    `PseudoMetricSpace.le_two_mul_dist_ofPreNNDist`, hence the distance given by the former
+    pseudometric space structure is Lipschitz equivalent to the `d`. Thus the uniformities generated
+    by `d` and `dist` are equal. Since the former uniformity is equal to `𝓤 X`, the latter is equal
+    to `𝓤 X` as well. -/
   obtain ⟨U, hU_symm, hU_comp, hB⟩ :
     ∃ U : ℕ → SetRel X X,
       (∀ n, (U n).IsSymm) ∧

Mathlib/Topology/OpenPartialHomeomorph/Constructions.lean

@@ -127,7 +127,7 @@ theorem prod_symm_trans_prod
 end Prod
 
 /-!
-# Pi types
+## Pi types
 
 Finite indexed products of partial homeomorphisms
 -/

Mathlib/Topology/OpenPartialHomeomorph/IsImage.lean

@@ -269,7 +269,7 @@ theorem restr_source_inter (s : Set X) : e.restr (e.source ∩ s) = e.restr s :=
 end restrOpen
 
 /-!
-# ofSet
+## ofSet
 
 The identity on a set `s`
 -/

Mathlib/Topology/UniformSpace/AbstractCompletion.lean

@@ -12,13 +12,13 @@ public import Mathlib.Topology.UniformSpace.Equiv
 # Abstract theory of Hausdorff completions of uniform spaces
 
 This file characterizes Hausdorff completions of a uniform space α as complete Hausdorff spaces
-equipped with a map from α which has dense image and induce the original uniform structure on α.
+equipped with a map from α which has dense image and induces the original uniform structure on α.
 Assuming these properties we "extend" uniformly continuous maps from α to complete Hausdorff spaces
 to the completions of α. This is the universal property expected from a completion.
 It is then used to extend uniformly continuous maps from α to α' to maps between
 completions of α and α'.
 
-This file does not construct any such completion, it only study consequences of their existence.
+This file does not construct any such completion; it only studies consequences of their existence.
 The first advantage is that formal properties are clearly highlighted without interference from
 construction details. The second advantage is that this framework can then be used to compare
 different completion constructions. See `Topology/UniformSpace/CompareReals` for an example.