typos from Bernardo Subercaseaux

avigad · Jan 20, 2025 · 024eeab · 024eeab
1 parent a620fcf
commit 024eeab
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 6 deletions.
diff --git a/MIL/C01_Introduction/S02_Overview.lean b/MIL/C01_Introduction/S02_Overview.lean
@@ -219,13 +219,13 @@ Marc Huisinga,
 Benjamin Jones,
 Julian Külshammer,
 Victor Liu, Jimmy Lu,
-Martin C. Martin, Giovanni Mascellani, John McDowell, Bhavik Mehta, Isaiah Mindich,
+Martin C. Martin, Giovanni Mascellani, John McDowell, Joseph McKinsey, Bhavik Mehta, Isaiah Mindich,
 Kabelo Moiloa, Hunter Monroe, Pietro Monticone,
 Oliver Nash, Emanuelle Natale, Filippo A. E. Nuccio,
 Pim Otte,
 Bartosz Piotrowski,
 Nicolas Rolland, Keith Rush,
-Yannick Seurin, Guilherme Silva,
+Yannick Seurin, Guilherme Silva, Bernardo Subercaseaux,
 Pedro Sánchez Terraf, Matthew Toohey, Alistair Tucker,
 Floris van Doorn,
 Eric Wieser,

diff --git a/MIL/C04_Sets_and_Functions/S01_Sets.lean b/MIL/C04_Sets_and_Functions/S01_Sets.lean
@@ -459,7 +459,7 @@ and anonymous constructors,
 these two expressions behave roughly the same.
 As a result, we usually don't need to use ``bex_def``
 to transform them explicitly.
-Here is are some examples of how they are used:
+Here are some examples of how they are used:
 TEXT. -/
 -- BOTH:
 section

diff --git a/MIL/C04_Sets_and_Functions/S02_Functions.lean b/MIL/C04_Sets_and_Functions/S02_Functions.lean
@@ -407,7 +407,7 @@ to their full domain,
 there are often relativized versions that restrict
 the statements to a subset of the domain type.
 
-Here is are some examples of ``InjOn`` and ``range`` in use:
+Here are some examples of ``InjOn`` and ``range`` in use:
 BOTH: -/
 section
 

diff --git a/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean b/MIL/C05_Elementary_Number_Theory/S02_Induction_and_Recursion.lean
@@ -175,7 +175,7 @@ The codomain of ``f`` can be any type that supports a commutative,
 associative addition operation with a zero element.
 If you import ``Algebra.BigOperators.Basic`` and issue the command
 ``open BigOperators``, you can use the more suggestive notation
-``∑ x in s, f x``. Of course, there is are an analogous operation and
+``∑ x in s, f x``. Of course, there is an analogous operation and
 notation for finite products.
 
 We will talk about the ``Finset`` type and the operations

diff --git a/MIL/C07_Hierarchies/S01_Basics.lean b/MIL/C07_Hierarchies/S01_Basics.lean
@@ -762,7 +762,6 @@ that every preorder comes with a ``<₁`` which has a default value built from `
 TEXT. -/
 
 -- SOLUTIONS:
-
 class LT₁ (α : Type) where
   /-- The Less-Than relation -/
   lt : α → α → Prop