From 6b81b191e742558ca70d1ad80645de2ff5c37ea1 Mon Sep 17 00:00:00 2001 From: Yannick Seurin Date: Thu, 6 Jun 2024 15:11:37 +0200 Subject: [PATCH] batch of typos --- MIL/C03_Logic/S03_Negation.lean | 2 +- MIL/C03_Logic/S04_Conjunction_and_Iff.lean | 2 +- MIL/C03_Logic/S05_Disjunction.lean | 7 +++---- 3 files changed, 5 insertions(+), 6 deletions(-) diff --git a/MIL/C03_Logic/S03_Negation.lean b/MIL/C03_Logic/S03_Negation.lean index 4c9ca9f1..fb55e430 100644 --- a/MIL/C03_Logic/S03_Negation.lean +++ b/MIL/C03_Logic/S03_Negation.lean @@ -91,7 +91,7 @@ example (h : ∀ a, ∃ x, f x > a) : ¬FnHasUb f := by /- TEXT: Remember that it is often convenient to use ``linarith`` when a goal follows from linear equations and -inequalities that in the context. +inequalities that are in the context. See if you can prove these in a similar way: TEXT. -/ diff --git a/MIL/C03_Logic/S04_Conjunction_and_Iff.lean b/MIL/C03_Logic/S04_Conjunction_and_Iff.lean index 6b7f604b..68c49f5c 100644 --- a/MIL/C03_Logic/S04_Conjunction_and_Iff.lean +++ b/MIL/C03_Logic/S04_Conjunction_and_Iff.lean @@ -190,7 +190,7 @@ You have already seen that you can write ``h.mp`` and ``h.mpr`` or ``h.1`` and ``h.2`` for the two directions of ``h : A ↔ B``. You can also use ``cases`` and friends. To prove an if-and-only-if statement, -you can uses ``constructor`` or angle brackets, +you can use ``constructor`` or angle brackets, just as you would if you were proving a conjunction. TEXT. -/ -- QUOTE: diff --git a/MIL/C03_Logic/S05_Disjunction.lean b/MIL/C03_Logic/S05_Disjunction.lean index 46475b9b..daacb17d 100644 --- a/MIL/C03_Logic/S05_Disjunction.lean +++ b/MIL/C03_Logic/S05_Disjunction.lean @@ -114,7 +114,7 @@ example : x < |y| → x < y ∨ x < -y := by /- TEXT: The names ``inl`` and ``inr`` are short for "intro left" and "intro right," -respectively. Using ``case`` has the advantage is that you can prove the +respectively. Using ``case`` has the advantage that you can prove the cases in either order; Lean uses the tag to find the relevant goal. If you don't care about that, you can use ``next``, or ``match``, or even a pattern-matching ``have``. @@ -129,7 +129,6 @@ example : x < |y| → x < y ∨ x < -y := by rw [abs_of_neg h] intro h; right; exact h - example : x < |y| → x < y ∨ x < -y := by match le_or_gt 0 y with | Or.inl h => @@ -141,12 +140,12 @@ example : x < |y| → x < y ∨ x < -y := by -- QUOTE. /- TEXT: -In the case of the ``match``, we need to use the full names +In the case of ``match``, we need to use the full names ``Or.inl`` and ``Or.inr`` of the canonical ways to prove a disjunction. In this textbook, we will generally use ``rcases`` to split on the cases of a disjunction. -Try proving the triangle inequality using the two +Try proving the triangle inequality using the first two theorems in the next snippet. They are given the same names they have in Mathlib. TEXT. -/