doc(Topology): tidy backticks (leanprover-community#31798)

Found and fixed with help from Codex.

Author: harahu

Mathlib/Topology/Algebra/InfiniteSum/Defs.lean

@@ -87,7 +87,7 @@ These are defined in an identical way to infinite sums (`HasSum`). For example,
 the function `ℕ → ℝ` sending `n` to `1 / 2` has a product of `0`, rather than saying that it does
 not converge as some authors would. -/
 @[to_additive /-- `HasSum f a L` means that the (potentially infinite) sum of the `f b` for `b : β`
-converges to `a` along the SummationFilter `L``.
+converges to `a` along the SummationFilter `L`.
 
 By default `L` is the `unconditional` one, corresponding to the limit of all finite sets towards
 the entire type. So we take the sum over bigger and bigger finite sets. This sum operation is

Mathlib/Topology/Algebra/IsUniformGroup/Constructions.lean

@@ -79,7 +79,7 @@ end PiProd
 
 section DiscreteUniformity
 
-/-- The discrete uniformity makes a group a `IsUniformGroup. -/
+/-- The discrete uniformity makes a group a `IsUniformGroup`. -/
 @[to_additive /-- The discrete uniformity makes an additive group a `IsUniformAddGroup`. -/]
 instance [UniformSpace G] [DiscreteUniformity G] : IsUniformGroup G where
   uniformContinuous_div := DiscreteUniformity.uniformContinuous (G × G) fun p ↦ p.1 / p.2

Mathlib/Topology/CompactOpen.lean

@@ -409,7 +409,7 @@ theorem curry_apply (f : C(X × Y, Z)) (a : X) (b : Y) : f.curry a b = f (a, b)
   rfl
 
 /-- To show continuity of a map `α → C(β, γ)`, it suffices to show that its uncurried form
-α × β → γ` is continuous. -/
+`α × β → γ` is continuous. -/
 theorem continuous_of_continuous_uncurry (f : X → C(Y, Z))
     (h : Continuous (Function.uncurry fun x y => f x y)) : Continuous f :=
   (curry ⟨_, h⟩).2

Mathlib/Topology/Constructions.lean

@@ -249,7 +249,7 @@ def CofiniteTopology (X : Type*) := X
 
 namespace CofiniteTopology
 
-/-- The identity equivalence between `` and `CofiniteTopology `. -/
+/-- The identity equivalence between `X` and `CofiniteTopology X`. -/
 def of : X ≃ CofiniteTopology X :=
   Equiv.refl X
 

Mathlib/Topology/ContinuousOn.lean

@@ -290,7 +290,7 @@ theorem ContinuousWithinAt.diff_iff
     h.mono diff_subset⟩
 
 /-- See also `continuousWithinAt_diff_singleton` for the case of `s \ {y}`, but
-requiring `T1Space α. -/
+requiring `T1Space α`. -/
 @[simp]
 theorem continuousWithinAt_diff_self :
     ContinuousWithinAt f (s \ {x}) x ↔ ContinuousWithinAt f s x :=

Mathlib/Topology/MetricSpace/DilationEquiv.lean

@@ -10,7 +10,7 @@ public import Mathlib.Topology.MetricSpace.Dilation
 /-!
 # Dilation equivalence
 
-In this file we define `DilationEquiv X Y`, a type of bundled equivalences between `X` and Y` such
+In this file we define `DilationEquiv X Y`, a type of bundled equivalences between `X` and `Y` such
 that `edist (f x) (f y) = r * edist x y` for some `r : ℝ≥0`, `r ≠ 0`.
 
 We also develop basic API about these equivalences.

Mathlib/Topology/MetricSpace/PiNat.lean

@@ -937,7 +937,7 @@ variable [∀ i, MetricSpace (F i)]
 /-- Given a countable family of metric spaces, one may put a distance on their product `Π i, E i`.
 
 It is highly non-canonical, though, and therefore not registered as a global instance.
-The distance we use here is edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i))`. -/
+The distance we use here is `edist x y = ∑' i, min (1/2)^(encode i) (edist (x i) (y i))`. -/
 protected def metricSpace : MetricSpace (∀ i, F i) :=
   EMetricSpace.toMetricSpaceOfDist dist (by simp) (by simp [edist_dist])
 

Mathlib/Topology/Order/OrderClosed.lean

@@ -28,8 +28,8 @@ We prove many basic properties of such topologies.
 
 This file contains the proofs of the following facts.
 For exact requirements
-(`OrderClosedTopology` vs `ClosedIciTopology` vs `ClosedIicTopology,
-`Preorder` vs `PartialOrder` vs `LinearOrder` etc)
+(`OrderClosedTopology` vs `ClosedIciTopology` vs `ClosedIicTopology`,
+`Preorder` vs `PartialOrder` vs `LinearOrder`, etc.)
 see their statements.
 
 ### Open / closed sets

Mathlib/Topology/VectorBundle/Riemannian.lean

@@ -380,7 +380,7 @@ structure RiemannianMetric where
   continuousAt (b : B) : ContinuousAt (fun (v : E b) ↦ inner b v v) 0
   isVonNBounded (b : B) : IsVonNBounded ℝ {v : E b | inner b v v < 1}
 
-/-- `Core structure associated to a family of inner products on the fibers of a fiber bundle. This
+/-- `Core` structure associated to a family of inner products on the fibers of a fiber bundle. This
 is an auxiliary construction to endow the fibers with an inner product space structure without
 creating diamonds.