diff --git a/MIL/C01_Introduction/S02_Overview.lean b/MIL/C01_Introduction/S02_Overview.lean index 587aeb7..552005f 100644 --- a/MIL/C01_Introduction/S02_Overview.lean +++ b/MIL/C01_Introduction/S02_Overview.lean @@ -65,7 +65,7 @@ Lean accepts it as a term of that type, you have done something very impressive. (Using ``sorry`` is cheating, and Lean knows it.) So now you know the game. -All that is left to learn are the rules. +All that is left to learn is the rules. This book is complementary to a companion tutorial, `Theorem Proving in Lean `_, diff --git a/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean b/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean index 1e916ec..8d0067d 100644 --- a/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean +++ b/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean @@ -470,7 +470,7 @@ If ``x`` has type ``α`` and ``s`` has type ``Set α``, then ``x ∈ s`` is a pr that asserts that ``x`` is an element of ``s``. If ``y`` has some different type ``β`` then the expression ``y ∈ s`` makes no sense. Here "makes no sense" means "has no type hence Lean does not accept it as a well-formed statement". This contrasts with Zermelo-Fraenkel set theory for instance -where ``a ∈ b`` is a well-formed statement for every mathematical objects ``a`` and ``b``. +where ``a ∈ b`` is a well-formed statement for both mathematical objects ``a`` and ``b``. For instance ``sin ∈ cos`` is a well-formed statement in ZF. This defect of set theoretic foundations is an important motivation for not using it in a proof assistant which is meant to assist us by detecting meaningless expressions. In Lean ``sin`` has type ``ℝ → ℝ`` and ``cos`` has type diff --git a/MIL/C04_Sets_and_Functions/S01_Sets.lean b/MIL/C04_Sets_and_Functions/S01_Sets.lean index 2233a88..22707d7 100644 --- a/MIL/C04_Sets_and_Functions/S01_Sets.lean +++ b/MIL/C04_Sets_and_Functions/S01_Sets.lean @@ -328,7 +328,7 @@ In type theory, a *property* or *predicate* on a type ``α`` is just a function ``P : α → Prop``. This makes sense: given ``a : α``, ``P a`` is just the proposition -that ``P`` holds of ``a``. +that ``P`` holds for ``a``. In the library, ``Set α`` is defined to be ``α → Prop`` and ``x ∈ s`` is defined to be ``s x``. In other words, sets are really properties, treated as objects.