24319619 - mathematics_in_lean

Authored by: Jeremy Avigad
Authored at: 2023-06-09 09:44:34 -0700
Committed by: Jeremy Avigad
Committed at: 2023-06-09 09:44:34 -0700
Object name: 2431961906f4a240163716f7f930a28948707033
Parent: f38ac68b

Update Fri Jun 9 09:44:34 PDT 2023

Changes

64 changed files (+41/-6)

.gitignore
- @@ -1,4 +1,5 @@
  /.vscode - *.olean - /_target - /leanpkg.path + /build + /lake-packages + /.cache + .DS_Store
MIL.lean (new)
- @@ -0,0 +1,34 @@
  + import MIL.C01_Introduction.S01_Getting_Started + import MIL.C01_Introduction.S02_Overview + import MIL.C02_Basics.S01_Calculating + import MIL.C02_Basics.S02_Proving_Identities_in_Algebraic_Structures + import MIL.C02_Basics.S03_Using_Theorems_and_Lemmas + import MIL.C02_Basics.S04_More_on_Order_and_Divisibility + import MIL.C02_Basics.S05_Proving_Facts_about_Algebraic_Structures + import MIL.C03_Logic.S01_Implication_and_the_Universal_Quantifier + import MIL.C03_Logic.S02_The_Existential_Quantifier + import MIL.C03_Logic.S03_Negation + import MIL.C03_Logic.«S04_Conjunction_and_Bi-implication» + import MIL.C03_Logic.S05_Disjunction + import MIL.C03_Logic.S06_Sequences_and_Convergence + import MIL.C04_Sets_and_Functions.S01_Sets + import MIL.C04_Sets_and_Functions.S02_Functions + import MIL.C04_Sets_and_Functions.S03_The_Schroeder_Bernstein_Theorem + import MIL.C05_Number_Theory.S01_Irrational_Roots + import MIL.C05_Number_Theory.S02_Induction_and_Recursion + import MIL.C05_Number_Theory.S03_Infinitely_Many_Primes + import MIL.C06_Structures.S01_Structures + import MIL.C06_Structures.S02_Algebraic_Structures + import MIL.C06_Structures.S03_Building_the_Gaussian_Integers + import MIL.C07_Hierarchies.S01_Basics + import MIL.C07_Hierarchies.S02_Morphisms + import MIL.C07_Hierarchies.S03_Subobjects + import MIL.C08_Topology.S01_Filters + import MIL.C08_Topology.S02_Metric_Spaces + import MIL.C08_Topology.S03_Topological_Spaces + import MIL.C09_Differential_Calculus.S01_Elementary_Differential_Calculus + import MIL.C09_Differential_Calculus.S02_Differential_Calculus_in_Normed_Spaces + + --import MIL.C10_Integration_and_Measure_Theory.S01_Elementary_Integration + --import MIL.C10_Integration_and_Measure_Theory.S02_Measure_Theory + --import MIL.C10_Integration_and_Measure_Theory.S03_Integration
src/C01_Introduction/S01_Getting_Started.lean > MIL/C01_Introduction/S01_Getting_Started.lean
src/C01_Introduction/S02_Overview.lean > MIL/C01_Introduction/S02_Overview.lean
src/C01_Introduction/solutions/Solutions_S01_Getting_Started.lean > MIL/C01_Introduction/solutions/Solutions_S01_Getting_Started.lean
src/C01_Introduction/solutions/Solutions_S02_Overview.lean > MIL/C01_Introduction/solutions/Solutions_S02_Overview.lean
src/C02_Basics/S01_Calculating.lean > MIL/C02_Basics/S01_Calculating.lean
src/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean > MIL/C02_Basics/S02_Proving_Identities_in_Algebraic_Structures.lean
src/C02_Basics/S03_Using_Theorems_and_Lemmas.lean > MIL/C02_Basics/S03_Using_Theorems_and_Lemmas.lean
src/C02_Basics/S04_More_on_Order_and_Divisibility.lean > MIL/C02_Basics/S04_More_on_Order_and_Divisibility.lean
src/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean > MIL/C02_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean
src/C02_Basics/solutions/Solutions_S01_Calculating.lean > MIL/C02_Basics/solutions/Solutions_S01_Calculating.lean
src/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean > MIL/C02_Basics/solutions/Solutions_S02_Proving_Identities_in_Algebraic_Structures.lean
src/C02_Basics/solutions/Solutions_S03_Using_Theorems_and_Lemmas.lean > MIL/C02_Basics/solutions/Solutions_S03_Using_Theorems_and_Lemmas.lean
src/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean > MIL/C02_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean
src/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean > MIL/C02_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean
src/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean > MIL/C03_Logic/S01_Implication_and_the_Universal_Quantifier.lean
src/C03_Logic/S02_The_Existential_Quantifier.lean > MIL/C03_Logic/S02_The_Existential_Quantifier.lean
src/C03_Logic/S03_Negation.lean > MIL/C03_Logic/S03_Negation.lean
src/C03_Logic/S04_Conjunction_and_Bi-implication.lean > MIL/C03_Logic/S04_Conjunction_and_Bi-implication.lean
src/C03_Logic/S05_Disjunction.lean > MIL/C03_Logic/S05_Disjunction.lean
src/C03_Logic/S06_Sequences_and_Convergence.lean > MIL/C03_Logic/S06_Sequences_and_Convergence.lean
src/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean > MIL/C03_Logic/solutions/Solutions_S01_Implication_and_the_Universal_Quantifier.lean
src/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean > MIL/C03_Logic/solutions/Solutions_S02_The_Existential_Quantifier.lean
src/C03_Logic/solutions/Solutions_S03_Negation.lean > MIL/C03_Logic/solutions/Solutions_S03_Negation.lean
src/C03_Logic/solutions/Solutions_S04_Conjunction_and_Bi-implication.lean > MIL/C03_Logic/solutions/Solutions_S04_Conjunction_and_Bi-implication.lean
src/C03_Logic/solutions/Solutions_S05_Disjunction.lean > MIL/C03_Logic/solutions/Solutions_S05_Disjunction.lean
src/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean > MIL/C03_Logic/solutions/Solutions_S06_Sequences_and_Convergence.lean
src/C04_Sets_and_Functions/S01_Sets.lean > MIL/C04_Sets_and_Functions/S01_Sets.lean
src/C04_Sets_and_Functions/S02_Functions.lean > MIL/C04_Sets_and_Functions/S02_Functions.lean
src/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean > MIL/C04_Sets_and_Functions/S03_The_Schroeder_Bernstein_Theorem.lean
src/C04_Sets_and_Functions/solutions/Solutions_S01_Sets.lean > MIL/C04_Sets_and_Functions/solutions/Solutions_S01_Sets.lean
src/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean > MIL/C04_Sets_and_Functions/solutions/Solutions_S02_Functions.lean
src/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean > MIL/C04_Sets_and_Functions/solutions/Solutions_S03_The_Schroeder_Bernstein_Theorem.lean
src/C05_Number_Theory/S01_Irrational_Roots.lean > MIL/C05_Number_Theory/S01_Irrational_Roots.lean
src/C05_Number_Theory/S02_Induction_and_Recursion.lean > MIL/C05_Number_Theory/S02_Induction_and_Recursion.lean
src/C05_Number_Theory/S03_Infinitely_Many_Primes.lean > MIL/C05_Number_Theory/S03_Infinitely_Many_Primes.lean
src/C05_Number_Theory/solutions/Solutions_S01_Irrational_Roots.lean > MIL/C05_Number_Theory/solutions/Solutions_S01_Irrational_Roots.lean
src/C05_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean > MIL/C05_Number_Theory/solutions/Solutions_S02_Induction_and_Recursion.lean
src/C05_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean > MIL/C05_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean
src/C06_Structures/S01_Structures.lean > MIL/C06_Structures/S01_Structures.lean
src/C06_Structures/S02_Algebraic_Structures.lean > MIL/C06_Structures/S02_Algebraic_Structures.lean
src/C06_Structures/S03_Building_the_Gaussian_Integers.lean > MIL/C06_Structures/S03_Building_the_Gaussian_Integers.lean
src/C06_Structures/solutions/Solutions_S01_Structures.lean > MIL/C06_Structures/solutions/Solutions_S01_Structures.lean
src/C06_Structures/solutions/Solutions_S02_Algebraic_Structures.lean > MIL/C06_Structures/solutions/Solutions_S02_Algebraic_Structures.lean
src/C06_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean > MIL/C06_Structures/solutions/Solutions_S03_Building_the_Gaussian_Integers.lean
src/C07_Hierarchies/S01_Basics.lean > MIL/C07_Hierarchies/S01_Basics.lean
src/C07_Hierarchies/S02_Morphisms.lean > MIL/C07_Hierarchies/S02_Morphisms.lean
src/C07_Hierarchies/S03_Subobjects.lean > MIL/C07_Hierarchies/S03_Subobjects.lean
src/C07_Hierarchies/solutions/Solutions_S01_Basics.lean > MIL/C07_Hierarchies/solutions/Solutions_S01_Basics.lean
src/C07_Hierarchies/solutions/Solutions_S02_Morphisms.lean > MIL/C07_Hierarchies/solutions/Solutions_S02_Morphisms.lean
src/C07_Hierarchies/solutions/Solutions_S03_Subobjects.lean > MIL/C07_Hierarchies/solutions/Solutions_S03_Subobjects.lean
src/C08_Topology/S01_Filters.lean > MIL/C08_Topology/S01_Filters.lean
src/C08_Topology/S02_Metric_Spaces.lean > MIL/C08_Topology/S02_Metric_Spaces.lean
src/C08_Topology/S03_Topological_Spaces.lean > MIL/C08_Topology/S03_Topological_Spaces.lean
src/C08_Topology/solutions/Solutions_S01_Filters.lean > MIL/C08_Topology/solutions/Solutions_S01_Filters.lean
src/C08_Topology/solutions/Solutions_S02_Metric_Spaces.lean > MIL/C08_Topology/solutions/Solutions_S02_Metric_Spaces.lean
src/C08_Topology/solutions/Solutions_S03_Topological_Spaces.lean > MIL/C08_Topology/solutions/Solutions_S03_Topological_Spaces.lean
src/C09_Differential_Calculus/S01_Elementary_Differential_Calculus.lean > MIL/C09_Differential_Calculus/S01_Elementary_Differential_Calculus.lean
src/C09_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean > MIL/C09_Differential_Calculus/S02_Differential_Calculus_in_Normed_Spaces.lean
src/C09_Differential_Calculus/solutions/Solutions_S01_Elementary_Differential_Calculus.lean > MIL/C09_Differential_Calculus/solutions/Solutions_S01_Elementary_Differential_Calculus.lean
src/C09_Differential_Calculus/solutions/Solutions_S02_Differential_Calculus_in_Normed_Spaces.lean > MIL/C09_Differential_Calculus/solutions/Solutions_S02_Differential_Calculus_in_Normed_Spaces.lean
README.md
- @@ -48,7 +48,7 @@ You can open the book in a side panel in VS Code as follows:
  Each section in the book has an associated Lean file with examples and exercises. - You can find them in the folder `src`, organized by chapter. + You can find them in the folder `MIL`, organized by chapter. We recommend making a copy of that folder, naming it something like `my_files`. That way you can experiment with the files as you go
- @@ -60,7 +60,7 @@ and read the book in VS Code while you work on the exercises.
  You can update to a newer version of this repository by typing ``git pull`` followed by ``lake exe cache get`` inside the ``mathematics_in_lean`` folder. - This will update the `src` folder, but will not change `my_files`. + This will update the `MIL` folder, but will not change `my_files`. ## To use this repository with Gitpod
- @@ -70,7 +70,7 @@ This creates a virtual machine in the cloud,
  and installs Lean and mathlib. It then presents you with a VS Code window, running in a virtual copy of the repository. - You can then make a copy of the `src` directory, and so on, + You can then make a copy of the `MIL` directory, and so on, following the instructions above. Gitpod gives you 50 free hours every month.
mathematics_in_lean.pdf