From 5412d02a82f3b1f643b76a4a5ab07f683dc72ce5 Mon Sep 17 00:00:00 2001 From: euprunin Date: Wed, 23 Oct 2024 20:31:47 +0200 Subject: [PATCH] chore: remove redundant spacing --- MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean | 2 +- MIL/C03_Logic/S03_Negation.lean | 2 +- .../S03_The_Schroeder_Bernstein_Theorem.lean | 2 +- MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean | 2 +- .../S03_Infinitely_Many_Primes.lean | 2 +- MIL/C10_Topology/S01_Filters.lean | 2 +- MIL/C10_Topology/S03_Topological_Spaces.lean | 2 +- user_repo_source/.github/pull_request_template.md | 2 +- user_repo_source/README.md | 2 +- 9 files changed, 9 insertions(+), 9 deletions(-) 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 90ba8847..5c83ce44 100644 --- a/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean +++ b/MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean @@ -87,7 +87,7 @@ end At this stage, you also know that if you use the ``apply`` tactic to apply ``my_lemma`` to a goal of the form ``|a * b| < δ``, -you are left with new goals that require you to prove +you are left with new goals that require you to prove each of the hypotheses. .. index:: intro, tactics; intro diff --git a/MIL/C03_Logic/S03_Negation.lean b/MIL/C03_Logic/S03_Negation.lean index fb55e430..eda28a60 100644 --- a/MIL/C03_Logic/S03_Negation.lean +++ b/MIL/C03_Logic/S03_Negation.lean @@ -381,7 +381,7 @@ example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by -- SOLUTIONS: example (h : ¬Monotone f) : ∃ x y, x ≤ y ∧ f y < f x := by rw [Monotone] at h - push_neg at h + push_neg at h exact h /- TEXT: diff --git a/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean b/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean index 136799a3..d78e8f53 100644 --- a/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean +++ b/MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean @@ -266,7 +266,7 @@ SOLUTIONS: -/ rw [if_pos x₁A, if_pos x₂A] at hxeq exact hf hxeq -- BOTH: - push_neg at xA + push_neg at xA /- EXAMPLES: sorry SOLUTIONS: -/ diff --git a/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean b/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean index 1d96c49d..3bd1bddd 100644 --- a/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean +++ b/MIL/C05_Elementary_Number_Theory/S01_Irrational_Roots.lean @@ -465,5 +465,5 @@ end -- have := Ne.symm (ne_of_lt this) -- intro h -- field_simp [this] at h --- norm_cast at h +-- norm_cast at h -- sorry diff --git a/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean b/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean index 7fa7c8b7..d93e3e3c 100644 --- a/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean +++ b/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean @@ -142,7 +142,7 @@ SOLUTIONS: -/ refine ⟨p, ?_, pp⟩ show p > n by_contra ple - push_neg at ple + push_neg at ple have : p ∣ Nat.factorial (n + 1) := by /- EXAMPLES: sorry diff --git a/MIL/C10_Topology/S01_Filters.lean b/MIL/C10_Topology/S01_Filters.lean index 6f1316e8..757607cf 100644 --- a/MIL/C10_Topology/S01_Filters.lean +++ b/MIL/C10_Topology/S01_Filters.lean @@ -49,7 +49,7 @@ condition then says that ``univ`` is sufficiently large, the second one says tha large set is sufficiently large and the third one says that the intersection of two sufficiently large sets is sufficiently large. -It may be even more useful to think of a filter on a type ``X`` +It may be even more useful to think of a filter on a type ``X`` as a generalized element of ``Set X``. For instance, ``atTop`` is the "set of very large numbers" and ``𝓝 x₀`` is the "set of points very close to ``x₀``." One manifestation of this view is that we can associate to any ``s : Set X`` the so-called *principal filter* diff --git a/MIL/C10_Topology/S03_Topological_Spaces.lean b/MIL/C10_Topology/S03_Topological_Spaces.lean index f7efcc01..7b018da1 100644 --- a/MIL/C10_Topology/S03_Topological_Spaces.lean +++ b/MIL/C10_Topology/S03_Topological_Spaces.lean @@ -45,7 +45,7 @@ example {ι : Type*} [Fintype ι] {s : ι → Set X} (hs : ∀ i, IsOpen (s i)) /- TEXT: -Closed sets are then defined as sets whose complement is open. A function between topological spaces +Closed sets are then defined as sets whose complement is open. A function between topological spaces is (globally) continuous if all preimages of open sets are open. BOTH: -/ -- QUOTE: diff --git a/user_repo_source/.github/pull_request_template.md b/user_repo_source/.github/pull_request_template.md index 1301d3b2..70d565c5 100644 --- a/user_repo_source/.github/pull_request_template.md +++ b/user_repo_source/.github/pull_request_template.md @@ -1,3 +1,3 @@ WARNING: Please do not open a pull request in this repository. -This is not the relevant repository to contribute to Mathematics in Lean. This repository is cloned by people who want to study the book. It is automatically created from the source repository which can be found at https://github.com/avigad/mathematics_in_lean_source and where you can open a pull-request. +This is not the relevant repository to contribute to Mathematics in Lean. This repository is cloned by people who want to study the book. It is automatically created from the source repository which can be found at https://github.com/avigad/mathematics_in_lean_source and where you can open a pull-request. diff --git a/user_repo_source/README.md b/user_repo_source/README.md index ea0ffe1c..caa3a1e1 100644 --- a/user_repo_source/README.md +++ b/user_repo_source/README.md @@ -36,7 +36,7 @@ Do the following: You can call the copy `my_files` or whatever you want and use it to create your own Lean files as well. -At that point, you can open the textbook in a web browser +At that point, you can open the textbook in a web browser at [https://leanprover-community.github.io/mathematics_in_lean/](https://leanprover-community.github.io/mathematics_in_lean/) and start reading and doing the exercises in VS Code.