Fix a number of typos/grammar errors in the Topology chapter (#286)

Author: vlad902

MIL/C10_Topology/C10_Topology.rst

@@ -12,7 +12,7 @@ The notion of a *limit* is also fundamental.
 We may say that the limit of a function :math:`f(x)` is a value :math:`b`
 as :math:`x` approaches a value :math:`a`,
 or that :math:`f(x)` *converges to* :math:`b` as :math:`x` approaches :math:`a`.
-Equivalently, we may say that a :math:`f(x)` approaches :math:`b` as :math:`x`
+Equivalently, we may say that :math:`f(x)` approaches :math:`b` as :math:`x`
 approaches a value :math:`a`, or that it *tends to* :math:`b`
 as :math:`x` tends to :math:`a`.
 We have already begun to consider such notions in :numref:`sequences_and_convergence`.
@@ -22,7 +22,7 @@ Having covered the essentials of formalization in Chapters :numref:`%s <basics>`
 to :numref:`%s <structures>`,
 in this chapter, we will explain how topological notions are formalized in Mathlib.
 Not only do topological abstractions apply in much greater generality,
-but that also, somewhat paradoxically, make it easier to reason about limits
+but they also, somewhat paradoxically, make it easier to reason about limits
 and continuity in concrete instances.
 
 Topological notions build on quite a few layers of mathematical structure.
@@ -35,7 +35,7 @@ intermediate notion called a *uniform space*.
 
 Whereas previous chapters relied on mathematical notions that were likely
 familiar to you,
-the notion of a filter less well known,
+the notion of a filter is less well known,
 even to many working mathematicians.
 The notion is essential, however, for formalizing mathematics effectively.
 Let us explain why.

MIL/C10_Topology/S01_Filters.lean

@@ -108,9 +108,9 @@ We can also directly define the filter ``𝓝 x`` of neighborhoods of any ``x :
 In the real numbers, a neighborhood of ``x`` is a set containing an open interval
 :math:`(x_0 - \varepsilon, x_0 + \varepsilon)`,
 defined in Mathlib as ``Ioo (x₀ - ε) (x₀ + ε)``.
-(This is notion of a neighborhood is only a special case of a more general construction in Mathlib.)
+(This notion of a neighborhood is only a special case of a more general construction in Mathlib.)
 
-With these examples, we can already define what is means for a function ``f : X → Y``
+With these examples, we can already define what it means for a function ``f : X → Y``
 to converge to some ``G : Filter Y`` along some ``F : Filter X``,
 as follows:
 BOTH: -/
@@ -134,7 +134,7 @@ hide the quantifier ``∀ V`` and make the intuition more salient by using more
 The first ingredient is the *pushforward* operation :math:`f_*` associated to any map ``f : X → Y``,
 denoted ``Filter.map f`` in Mathlib. Given a filter ``F`` on ``X``, ``Filter.map f F : Filter Y`` is defined so that
 ``V ∈ Filter.map f F ↔ f ⁻¹' V ∈ F`` holds definitionally.
-In this examples file we've opened the ``Filter`` namespace so that
+In the example file we've opened the ``Filter`` namespace so that
 ``Filter.map`` can be written as ``map``. This means that we can rewrite the definition of ``Tendsto`` using
 the order relation on ``Filter Y``, which is reversed inclusion of the set of members.
 In other words, given ``G H : Filter Y``, we have ``G ≤ H ↔ ∀ V : Set Y, V ∈ H → V ∈ G``.

MIL/C10_Topology/S02_Metric_Spaces.lean

@@ -260,14 +260,14 @@ Compactness
 ^^^^^^^^^^^
 
 Compactness is an important topological notion. It distinguishes subsets of a metric space
-that enjoy the same kind of properties as segments in reals compared to other intervals:
+that enjoy the same kind of properties as segments in the reals compared to other intervals:
 
-* Any sequence taking value in a compact set has a subsequence that converges in this set
+* Any sequence with values in a compact set has a subsequence that converges in this set.
 * Any continuous function on a nonempty compact set with values in real numbers is bounded and
-  achieves its bounds somewhere (this is called the extreme values theorem).
+  attains its bounds somewhere (this is called the extreme value theorem).
 * Compact sets are closed sets.
 
-Let us first check that the unit interval in reals is indeed a compact set, and then check the above
+Let us first check that the unit interval in the reals is indeed a compact set, and then check the above
 claims for compact sets in general metric spaces. In the second statement we only
 need continuity on the given set so we will use ``ContinuousOn`` instead of ``Continuous``, and
 we will give separate statements for the minimum and the maximum. Of course all these results

MIL/C10_Topology/S03_Topological_Spaces.lean

@@ -82,7 +82,7 @@ example {f : X → Y} {x : X} : ContinuousAt f x ↔ map f (𝓝 x) ≤ 𝓝 (f
 /- TEXT:
 One can also spell it using both neighborhoods seen as ordinary sets and a neighborhood filter
 seen as a generalized set: "for any neighborhood ``U`` of ``f x``, all points close to ``x``
-are sent to ``U``". Note that the proof is again ``iff.rfl``, this point of view is definitionally
+are sent to ``U``". Note that the proof is again ``Iff.rfl``, this point of view is definitionally
 equivalent to the previous one.
 
 BOTH: -/
@@ -171,7 +171,7 @@ equivalently, it can be pulled back by an injective map. But that's pretty much
 They cannot be pulled back by general map or pushed forward, even by surjective maps.
 
 In particular there is no sensible distance to put on a quotient of a metric space or on an uncountable
-products of metric spaces. Consider for instance the type ``ℝ → ℝ``, seen as
+product of metric spaces. Consider for instance the type ``ℝ → ℝ``, seen as
 a product of copies of ``ℝ`` indexed by ``ℝ``. We would like to say that pointwise convergence of
 sequences of functions is a respectable notion of convergence. But there is no distance on
 ``ℝ → ℝ`` that gives this notion of convergence. Relatedly, there is no distance ensuring that