Cleaning chapter 9

MIL/C07_Hierarchies/S01_Basics.lean

@@ -27,9 +27,9 @@ more details about what the ``class`` command is doing.
 First, the ``class`` command above defines a structure ``One₁`` with parameter ``α : Type`` and
 a single field ``one``. It also mark this structure as a class so that arguments of type
 ``One₁ α`` for some type ``α`` will be inferrable using the instance resolution procedure,
-as long as they are marked as instance-implicit, ie appear between square brackets.
+as long as they are marked as instance-implicit, i.e. appear between square brackets.
 Those two effects could also have been achieved using the ``structure`` command with ``class``
-attribute, ie writing ``@[class] structure`` instance of ``class``. But the class command also
+attribute, i.e. writing ``@[class] structure`` instance of ``class``. But the class command also
 ensures that ``One₁ α`` appears as an instance-implicit argument in its own fields. Compare:
 BOTH: -/
 

MIL/C09_Linear_Algebra/S01_Vector_Spaces.lean

@@ -45,11 +45,11 @@ This would be very bad for the type class synthesis system.
 
 The multiplication of a vector `v` by a scalar `a` is denoted by
 `a • v`. We list a couple of algebraic rules about the interaction of this
-operation with addition in the following examples. Of course `simp` of `apply?`
+operation with addition in the following examples. Of course `simp` or `apply?`
 would find those proofs. There is also a `module` tactic that solves goals
 following from the axioms of vector spaces and fields, in the same way the
 `ring` tactic is used in commutative rings or the `group` tactic is used in
-groups. But it is still useful to remember than scalar
+groups. But it is still useful to remember that scalar
 multiplication is abbreviated `smul` in lemma names.
 
 
@@ -87,7 +87,7 @@ Linear maps
 
 .. index:: linear map
 
-Next we need linear maps. Like group morphisms, linear maps in Mathlib are bundled maps, ie packages
+Next we need linear maps. Like group morphisms, linear maps in Mathlib are bundled maps, i.e. packages
 made of a map and proofs of its linearity properties.
 Those bundled maps are converted to ordinary functions when applied.
 See :numref:`Chapter %s <hierarchies>` for more information about this design.
@@ -129,7 +129,7 @@ variable (ψ : V →ₗ[K] W)
 -- QUOTE.
 
 /- TEXT:
-One down-side of using bundled maps is that we cannot use ordinary function composition.
+One downside of using bundled maps is that we cannot use ordinary function composition.
 We need to use ``LinearMap.comp`` or the notation ``∘ₗ``.
 
 EXAMPLES: -/
@@ -161,7 +161,7 @@ You may wonder why the proof fields of ``LinearMap`` have names ending with a pr
 This is because they are defined before the coercion to functions is defined, hence they are
 phrased in terms of ``LinearMap.toFun``. Then they are restated as ``LinearMap.map_add``
 and ``LinearMap.map_smul`` in terms of the coercion to function.
-This is not yet the end of the story. One also want a version of ``map_add`` that applies to
+This is not yet the end of the story. One also wants a version of ``map_add`` that applies to
 any (bundled) map preserving addition, such as additive group morphisms, linear maps, continuous
 linear maps, ``K``-algebra maps etc… This one is ``map_add`` (in the root namespace).
 The intermediate version, ``LinearMap.map_add`` is a bit redundant but allows to use dot notation, which

MIL/C09_Linear_Algebra/S04_Bases.lean

@@ -106,7 +106,7 @@ EXAMPLES: -/
 /- TEXT:
 When entries do not have a computable type, for instance if they are real numbers, we cannot
 hope that ``#eval`` can help. Also this kind of evaluation cannot be used in proofs without
-considerably expanding the trusted code base (ie the part of Lean that you need to trust when
+considerably expanding the trusted code base (i.e. the part of Lean that you need to trust when
 checking proofs).
 
 So it is good to also use the ``simp`` and ``norm_num`` tactics in proofs, or
@@ -240,7 +240,7 @@ Indeed only finite linear combinations make sense in this algebraic context. So
 as a reference vector space is not a direct product of copies of ``K`` but a direct sum.
 We could use ``⨁ i : ι, K`` for some type ``ι`` indexing the basis
 But we rather use the more specialized spelling ``ι →₀ K`` which means
-“functions from ``ι`` to ``K`` with finite support”, ie functions which vanish outside a finite set
+“functions from ``ι`` to ``K`` with finite support”, i.e. functions which vanish outside a finite set
 in ``ι`` (this finite set is not fixed, it depends on the function).
 Evaluating such a function coming from a basis ``B`` at a vector ``v`` and
 ``i : ι`` returns the component (or coordinate) of ``v`` on the ``i``-th basis vector.
@@ -273,7 +273,7 @@ Instead of starting with such an isomorphism, one can start with a family ``b``
 linearly independent and spanning, this is ``Basis.mk``.
 
 The assumption that the family is spanning is spelled out as ``⊤ ≤ Submodule.span K (Set.range b)``.
-Here ``⊤`` is the top submodule of ``V``, ie ``V`` seen as submodule of itself.
+Here ``⊤`` is the top submodule of ``V``, i.e. ``V`` seen as submodule of itself.
 This spelling looks a bit tortuous, but we will see below that it is almost equivalent by definition
 to the more readable ``∀ v, v ∈ Submodule.span K (Set.range b)`` (the underscores in the snippet
 below refers to the useless information ``v ∈ ⊤``).
@@ -294,7 +294,7 @@ example (b : ι → V) (b_indep : LinearIndependent K b)
 In particular the model vector space ``ι →₀ K`` has a so-called canonical basis whose ``repr``
 function evaluated on any vector is the identity isomorphism. It is called
 ``Finsupp.basisSingleOne`` where ``Finsupp`` means function with finite support and
-``basisSingleOne`` refers to the fact that basis vectors are function which
+``basisSingleOne`` refers to the fact that basis vectors are functions which
 vanish expect for a single input value. More precisely the basis vector indexed by ``i : ι``
 is ``Finsupp.single i 1`` which is the finitely supported function taking value ``1`` at ``i``
 and ``0`` everywhere else.
@@ -374,7 +374,7 @@ variable (f : ι → V) in
 #check (Finsupp.linearCombination K f : (ι →₀ K) →ₗ[K] V)
 -- QUOTE.
 /- TEXT:
-The above subtlety also explain why dot notation cannot be used to write
+The above subtlety also explains why dot notation cannot be used to write
 ``c.linearCombination K f`` instead of ``Finsupp.linearCombination K f c``.
 Indeed ``Finsupp.linearCombination`` does not take ``c`` as an argument,
 ``Finsupp.linearCombination K f`` is coerced to a function type and then this function
@@ -551,7 +551,7 @@ The above spelling is strange because we already have ``h`` as an assumption, so
 just as well give the full proof ``FiniteDimensional.finrank_pos_iff.1 h`` but it
 is good to know for more complicated cases.
 
-By definition, ``FiniteDimensional K V`` can be read from any basis.
+By definition, ``FiniteDimensional K V`` can be read from any basis.
 EXAMPLES: -/
 -- QUOTE:
 variable {ι : Type*} (B : Basis ι K V)
@@ -605,7 +605,7 @@ end
 Let us now move to the general case of dimension theory. In this case
 ``finrank`` is useless, but we still have that, for any two bases of the same
 vector space, there is a bijection between the types indexing those bases. So we
-can still hope to define the rank as a cardinal, ie an element of the “quotient of
+can still hope to define the rank as a cardinal, i.e. an element of the “quotient of
 the collection of types under the existence of a bijection equivalence
 relation”.
 
@@ -625,8 +625,8 @@ by ``u + 1``, and ``Type u`` has type ``Type (u+1)``.
 But universe levels are not natural numbers, they have a really different nature and don’t
 have a type. In particular you cannot state in Lean something like ``u ≠ u + 1``.
 There is simply no type where this would take place. Even stating
-``Type u ≠ Type (u+1)`` does not make any sense since ``Type u`` and ``Type
-(u+1)`` have different types.
+``Type u ≠ Type (u+1)`` does not make any sense since ``Type u`` and ``Type (u+1)``
+have different types.
 
 Whenever we write ``Type*``, Lean inserts a universe level variable named ``u_n`` where ``n`` is a
 number. This allows definitions and statements to live in all universes.
@@ -640,7 +640,7 @@ denote a universe variable. The image of ``α : Type u`` in this quotient is
 But we cannot directly compare cardinals in different universes. So technically we
 cannot define the rank of a vector space ``V`` as the cardinal of all types indexing
 a basis of ``V``.
-So instead it is defined as the supremum ``Module.rank K V`` of cardinals of
+So instead it is defined as the supremum ``Module.rank K V`` of cardinals of
 all linearly independent sets in ``V``. If ``V`` has universe level ``u`` then
 its rank has type ``Cardinal.{u}``.
 

MIL/C10_Topology/S03_Topological_Spaces.lean

@@ -213,7 +213,7 @@ BOTH: -/
 
 Then the next big piece is a complete lattice structure on ``TopologicalSpace X``
 for any given structure. If you think of topologies as being primarily the data of open sets then you expect
-the order relation on ``TopologicalSpace X`` to come from ``Set (Set X)``, ie you expect ``t ≤ t'``
+the order relation on ``TopologicalSpace X`` to come from ``Set (Set X)``, i.e. you expect ``t ≤ t'``
 if a set ``u`` is open for ``t'`` as soon as it is open for ``t``. However we already know that Mathlib focuses
 on neighborhoods more than open sets so, for any ``x : X`` we want the map from topological spaces to neighborhoods
 ``fun T : TopologicalSpace X ↦ @nhds X T x`` to be order preserving.
@@ -375,7 +375,7 @@ Since ``Y`` is regular, it suffices to check that for every *closed* neighborhoo
 ``V'`` of ``φ x``, ``φ ⁻¹' V' ∈ 𝓝 x``.
 The limit assumption gives (through the auxiliary lemma above)
 some ``V ∈ 𝓝 x`` such ``IsOpen V ∧ (↑) ⁻¹' V ⊆ f ⁻¹' V'``.
-Since ``V ∈ 𝓝 x``, it suffices to prove ``V ⊆ φ ⁻¹' V'``, ie  ``∀ y ∈ V, φ y ∈ V'``.
+Since ``V ∈ 𝓝 x``, it suffices to prove ``V ⊆ φ ⁻¹' V'``, i.e.  ``∀ y ∈ V, φ y ∈ V'``.
 Let's fix ``y`` in ``V``. Because ``V`` is *open*, it is a neighborhood of ``y``.
 In particular ``(↑) ⁻¹' V ∈ comap (↑) (𝓝 y)`` and a fortiori ``f ⁻¹' V' ∈ comap (↑) (𝓝 y)``.
 In addition ``comap (↑) (𝓝 y) ≠ ⊥`` because ``A`` is dense.
@@ -443,7 +443,7 @@ a point ``x : X`` is a cluster point of ``F`` if ``F``, seen as a generalized se
 with the generalized set of points that are close to ``x``.
 
 Then we can say that a set ``s`` is compact if every nonempty generalized set ``F`` contained in ``s``,
-ie such that ``F ≤ 𝓟 s``, has a cluster point in ``s``.
+i.e. such that ``F ≤ 𝓟 s``, has a cluster point in ``s``.
 
 BOTH: -/
 -- QUOTE: