doc(Topology,Analysis): fix over-zealous replacement true/false -> Tr…

…ue/False (#11994)

in doc comments.
These are terms of type bool, hence should be (Bool.)true/false.

And correct a typo also caused in the same PR.

Mathlib/Analysis/BoxIntegral/Partition/Filter.lean

@@ -34,15 +34,15 @@ the corresponding integral, or in the proofs of its properties. We equip
 
 The structure `BoxIntegral.IntegrationParams` has 3 boolean fields with the following meaning:
 
-* `bRiemann`: the value `True` means that the filter corresponds to a Riemann-style integral, i.e.
+* `bRiemann`: the value `true` means that the filter corresponds to a Riemann-style integral, i.e.
   in the definition of integrability we require a constant upper estimate `r` on the size of boxes
-  of a tagged partition; the value `False` means that the estimate may depend on the position of the
+  of a tagged partition; the value `false` means that the estimate may depend on the position of the
   tag.
 
-* `bHenstock`: the value `True` means that we require that each tag belongs to its own closed box;
-  the value `False` means that we only require that tags belong to the ambient box.
+* `bHenstock`: the value `true` means that we require that each tag belongs to its own closed box;
+  the value `false` means that we only require that tags belong to the ambient box.
 
-* `bDistortion`: the value `True` means that `r` can depend on the maximal ratio of sides of the
+* `bDistortion`: the value `true` means that `r` can depend on the maximal ratio of sides of the
   same box of a partition. Presence of this case make quite a few proofs harder but we can prove the
   divergence theorem only for the filter `BoxIntegral.IntegrationParams.GP = ⊥ =
   {bRiemann := false, bHenstock := true, bDistortion := true}`.
@@ -183,15 +183,15 @@ open TaggedPrepartition
 /-- An `IntegrationParams` is a structure holding 3 boolean values used to define a filter to be
 used in the definition of a box-integrable function.
 
-* `bRiemann`: the value `True` means that the filter corresponds to a Riemann-style integral, i.e.
+* `bRiemann`: the value `true` means that the filter corresponds to a Riemann-style integral, i.e.
   in the definition of integrability we require a constant upper estimate `r` on the size of boxes
-  of a tagged partition; the value `False` means that the estimate may depend on the position of the
+  of a tagged partition; the value `false` means that the estimate may depend on the position of the
   tag.
 
-* `bHenstock`: the value `True` means that we require that each tag belongs to its own closed box;
-  the value `False` means that we only require that tags belong to the ambient box.
+* `bHenstock`: the value `true` means that we require that each tag belongs to its own closed box;
+  the value `false` means that we only require that tags belong to the ambient box.
 
-* `bDistortion`: the value `True` means that `r` can depend on the maximal ratio of sides of the
+* `bDistortion`: the value `true` means that `r` can depend on the maximal ratio of sides of the
   same box of a partition. Presence of this case makes quite a few proofs harder but we can prove
   the divergence theorem only for the filter `BoxIntegral.IntegrationParams.GP = ⊥ =
   {bRiemann := false, bHenstock := true, bDistortion := true}`.

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -770,7 +770,7 @@ end
 
 /-- The series `∑' n, x ^ n / n!` is summable of any `x : ℝ`. See also `expSeries_div_summable`
 for a version that also works in `ℂ`, and `NormedSpace.expSeries_summable'` for a version
-that works inany normed algebra over `ℝ` or `ℂ`. -/
+that works in any normed algebra over `ℝ` or `ℂ`. -/
 theorem Real.summable_pow_div_factorial (x : ℝ) : Summable (fun n ↦ x ^ n / n ! : ℕ → ℝ) := by
   -- We start with trivial estimates
   have A : (0 : ℝ) < ⌊‖x‖⌋₊ + 1 := zero_lt_one.trans_le (by simp)

Mathlib/Topology/Category/Profinite/Nobeling.lean

@@ -71,7 +71,7 @@ In this section we define the relevant projection maps and prove some compatibil
 ### Main definitions
 
 * Let `J : I → Prop`. Then `Proj J : (I → Bool) → (I → Bool)` is the projection mapping everything
-  that satisfies `J i` to itself, and everything else to `False`.
+  that satisfies `J i` to itself, and everything else to `false`.
 
 * The image of `C` under `Proj J` is denoted `π C J` and the corresponding map `C → π C J` is called
   `ProjRestrict`. If `J` implies `K` we have a map `ProjRestricts : π C K → π C J`.
@@ -83,7 +83,7 @@ In this section we define the relevant projection maps and prove some compatibil
 variable (J K L : I → Prop) [∀ i, Decidable (J i)] [∀ i, Decidable (K i)] [∀ i, Decidable (L i)]
 
 /--
-The projection mapping everything that satisfies `J i` to itself, and everything else to `False`
+The projection mapping everything that satisfies `J i` to itself, and everything else to `false`
 -/
 def Proj : (I → Bool) → (I → Bool) :=
   fun c i ↦ if J i then c i else false
@@ -1161,10 +1161,10 @@ variable {o : Ordinal} (hC : IsClosed C) (hsC : contained C (Order.succ o))
 
 section ExactSequence
 
-/-- The subset of `C` consisting of those elements whose `o`-th entry is `False`. -/
+/-- The subset of `C` consisting of those elements whose `o`-th entry is `false`. -/
 def C0 := C ∩ {f | f (term I ho) = false}
 
-/-- The subset of `C` consisting of those elements whose `o`-th entry is `True`. -/
+/-- The subset of `C` consisting of those elements whose `o`-th entry is `true`. -/
 def C1 := C ∩ {f | f (term I ho) = true}
 
 theorem isClosed_C0 : IsClosed (C0 C ho) := by
@@ -1198,7 +1198,7 @@ theorem contained_C' : contained (C' C ho) o := fun f hf i hi ↦ contained_C1 C
 
 variable (o)
 
-/-- Swapping the `o`-th coordinate to `True`. -/
+/-- Swapping the `o`-th coordinate to `true`. -/
 noncomputable
 def SwapTrue : (I → Bool) → I → Bool :=
   fun f i ↦ if ord I i = o then true else f i