diff --git a/MIL/C07_Hierarchies/S01_Basics.lean b/MIL/C07_Hierarchies/S01_Basics.lean index 04f05374..0db6c2e1 100644 --- a/MIL/C07_Hierarchies/S01_Basics.lean +++ b/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: -/ diff --git a/MIL/C09_Linear_Algebra/S01_Vector_Spaces.lean b/MIL/C09_Linear_Algebra/S01_Vector_Spaces.lean index 31ab1fc7..644a81c4 100644 --- a/MIL/C09_Linear_Algebra/S01_Vector_Spaces.lean +++ b/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 ` 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 diff --git a/MIL/C09_Linear_Algebra/S04_Bases.lean b/MIL/C09_Linear_Algebra/S04_Bases.lean index a9304a69..880e43ed 100644 --- a/MIL/C09_Linear_Algebra/S04_Bases.lean +++ b/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}``. diff --git a/MIL/C10_Topology/S03_Topological_Spaces.lean b/MIL/C10_Topology/S03_Topological_Spaces.lean index 8db6ab39..f7efcc01 100644 --- a/MIL/C10_Topology/S03_Topological_Spaces.lean +++ b/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: