From fdc5936766c37b8bfc7ef01059859a1903775286 Mon Sep 17 00:00:00 2001 From: Joshua Potter Date: Sat, 22 Apr 2023 14:28:15 -0600 Subject: [PATCH] Flatten directories, removing author packages. --- FirstCourseAbstractAlgebra.lean | 2 +- FirstCourseAbstractAlgebra/{Fraleigh => }/Chapter1.lean | 0 FirstCourseAbstractAlgebra/Fraleigh.lean | 1 - MathematicalIntroductionLogic.lean | 2 +- MathematicalIntroductionLogic/{Enderton => }/Chapter0.lean | 0 MathematicalIntroductionLogic/{Enderton => }/Chapter0.tex | 0 MathematicalIntroductionLogic/Enderton.lean | 1 - MockMockingbird.lean | 2 +- MockMockingbird/{Smullyan => }/Aviary.lean | 0 MockMockingbird/{Smullyan => }/Aviary.tex | 0 MockMockingbird/Smullyan.lean | 0 OneVariableCalculus.lean | 4 +++- OneVariableCalculus/Apostol.lean | 3 --- OneVariableCalculus/Apostol/Chapters.lean | 1 - OneVariableCalculus/Apostol/Exercises.lean | 1 - OneVariableCalculus/Apostol/Real.lean | 3 --- OneVariableCalculus/Apostol/Real/Function.lean | 1 - OneVariableCalculus/Apostol/Real/Geometry.lean | 3 --- OneVariableCalculus/Apostol/Real/Set.lean | 1 - OneVariableCalculus/Chapters.lean | 1 + .../{Apostol => }/Chapters/Chapter_I_3.lean | 0 OneVariableCalculus/{Apostol => }/Chapters/Chapter_I_3.tex | 0 OneVariableCalculus/Exercises.lean | 1 + .../{Apostol => }/Exercises/Exercises_1_7.lean | 0 .../{Apostol => }/Exercises/Exercises_I_3_12.lean | 2 +- OneVariableCalculus/Real.lean | 3 +++ OneVariableCalculus/Real/Function.lean | 1 + OneVariableCalculus/{Apostol => }/Real/Function/Step.lean | 2 +- OneVariableCalculus/Real/Geometry.lean | 3 +++ OneVariableCalculus/{Apostol => }/Real/Geometry/Area.lean | 4 ++-- OneVariableCalculus/{Apostol => }/Real/Geometry/Basic.lean | 0 .../{Apostol => }/Real/Geometry/Rectangle.lean | 2 +- OneVariableCalculus/Real/Set.lean | 1 + OneVariableCalculus/{Apostol => }/Real/Set/Partition.lean | 0 TheoremProvingInLean.lean | 7 ++++++- TheoremProvingInLean/Avigad.lean | 6 ------ TheoremProvingInLean/{Avigad => }/Chapter2.lean | 0 TheoremProvingInLean/{Avigad => }/Chapter3.lean | 0 TheoremProvingInLean/{Avigad => }/Chapter4.lean | 0 TheoremProvingInLean/{Avigad => }/Chapter5.lean | 0 TheoremProvingInLean/{Avigad => }/Chapter7.lean | 0 TheoremProvingInLean/{Avigad => }/Chapter8.lean | 0 42 files changed, 27 insertions(+), 31 deletions(-) rename FirstCourseAbstractAlgebra/{Fraleigh => }/Chapter1.lean (100%) delete mode 100644 FirstCourseAbstractAlgebra/Fraleigh.lean rename MathematicalIntroductionLogic/{Enderton => }/Chapter0.lean (100%) rename MathematicalIntroductionLogic/{Enderton => }/Chapter0.tex (100%) delete mode 100644 MathematicalIntroductionLogic/Enderton.lean rename MockMockingbird/{Smullyan => }/Aviary.lean (100%) rename MockMockingbird/{Smullyan => }/Aviary.tex (100%) delete mode 100644 MockMockingbird/Smullyan.lean delete mode 100644 OneVariableCalculus/Apostol.lean delete mode 100644 OneVariableCalculus/Apostol/Chapters.lean delete mode 100644 OneVariableCalculus/Apostol/Exercises.lean delete mode 100644 OneVariableCalculus/Apostol/Real.lean delete mode 100644 OneVariableCalculus/Apostol/Real/Function.lean delete mode 100644 OneVariableCalculus/Apostol/Real/Geometry.lean delete mode 100644 OneVariableCalculus/Apostol/Real/Set.lean create mode 100644 OneVariableCalculus/Chapters.lean rename OneVariableCalculus/{Apostol => }/Chapters/Chapter_I_3.lean (100%) rename OneVariableCalculus/{Apostol => }/Chapters/Chapter_I_3.tex (100%) create mode 100644 OneVariableCalculus/Exercises.lean rename OneVariableCalculus/{Apostol => }/Exercises/Exercises_1_7.lean (100%) rename OneVariableCalculus/{Apostol => }/Exercises/Exercises_I_3_12.lean (99%) create mode 100644 OneVariableCalculus/Real.lean create mode 100644 OneVariableCalculus/Real/Function.lean rename OneVariableCalculus/{Apostol => }/Real/Function/Step.lean (92%) create mode 100644 OneVariableCalculus/Real/Geometry.lean rename OneVariableCalculus/{Apostol => }/Real/Geometry/Area.lean (97%) rename OneVariableCalculus/{Apostol => }/Real/Geometry/Basic.lean (100%) rename OneVariableCalculus/{Apostol => }/Real/Geometry/Rectangle.lean (97%) create mode 100644 OneVariableCalculus/Real/Set.lean rename OneVariableCalculus/{Apostol => }/Real/Set/Partition.lean (100%) delete mode 100644 TheoremProvingInLean/Avigad.lean rename TheoremProvingInLean/{Avigad => }/Chapter2.lean (100%) rename TheoremProvingInLean/{Avigad => }/Chapter3.lean (100%) rename TheoremProvingInLean/{Avigad => }/Chapter4.lean (100%) rename TheoremProvingInLean/{Avigad => }/Chapter5.lean (100%) rename TheoremProvingInLean/{Avigad => }/Chapter7.lean (100%) rename TheoremProvingInLean/{Avigad => }/Chapter8.lean (100%) diff --git a/FirstCourseAbstractAlgebra.lean b/FirstCourseAbstractAlgebra.lean index 17778be..764aaee 100644 --- a/FirstCourseAbstractAlgebra.lean +++ b/FirstCourseAbstractAlgebra.lean @@ -1 +1 @@ -import FirstCourseAbstractAlgebra.Fraleigh \ No newline at end of file +import FirstCourseAbstractAlgebra.Chapter1 \ No newline at end of file diff --git a/FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean b/FirstCourseAbstractAlgebra/Chapter1.lean similarity index 100% rename from FirstCourseAbstractAlgebra/Fraleigh/Chapter1.lean rename to FirstCourseAbstractAlgebra/Chapter1.lean diff --git a/FirstCourseAbstractAlgebra/Fraleigh.lean b/FirstCourseAbstractAlgebra/Fraleigh.lean deleted file mode 100644 index 05d27be..0000000 --- a/FirstCourseAbstractAlgebra/Fraleigh.lean +++ /dev/null @@ -1 +0,0 @@ -import FirstCourseAbstractAlgebra.Fraleigh.Chapter1 diff --git a/MathematicalIntroductionLogic.lean b/MathematicalIntroductionLogic.lean index de93443..99394ed 100644 --- a/MathematicalIntroductionLogic.lean +++ b/MathematicalIntroductionLogic.lean @@ -1 +1 @@ -import MathematicalIntroductionLogic.Enderton \ No newline at end of file +import MathematicalIntroductionLogic.Chapter0 \ No newline at end of file diff --git a/MathematicalIntroductionLogic/Enderton/Chapter0.lean b/MathematicalIntroductionLogic/Chapter0.lean similarity index 100% rename from MathematicalIntroductionLogic/Enderton/Chapter0.lean rename to MathematicalIntroductionLogic/Chapter0.lean diff --git a/MathematicalIntroductionLogic/Enderton/Chapter0.tex b/MathematicalIntroductionLogic/Chapter0.tex similarity index 100% rename from MathematicalIntroductionLogic/Enderton/Chapter0.tex rename to MathematicalIntroductionLogic/Chapter0.tex diff --git a/MathematicalIntroductionLogic/Enderton.lean b/MathematicalIntroductionLogic/Enderton.lean deleted file mode 100644 index 3a2ee26..0000000 --- a/MathematicalIntroductionLogic/Enderton.lean +++ /dev/null @@ -1 +0,0 @@ -import MathematicalIntroductionLogic.Enderton.Chapter0 diff --git a/MockMockingbird.lean b/MockMockingbird.lean index 232c8ff..accd31b 100644 --- a/MockMockingbird.lean +++ b/MockMockingbird.lean @@ -1 +1 @@ -import MockMockingbird.Smullyan \ No newline at end of file +import MockMockingbird.Aviary \ No newline at end of file diff --git a/MockMockingbird/Smullyan/Aviary.lean b/MockMockingbird/Aviary.lean similarity index 100% rename from MockMockingbird/Smullyan/Aviary.lean rename to MockMockingbird/Aviary.lean diff --git a/MockMockingbird/Smullyan/Aviary.tex b/MockMockingbird/Aviary.tex similarity index 100% rename from MockMockingbird/Smullyan/Aviary.tex rename to MockMockingbird/Aviary.tex diff --git a/MockMockingbird/Smullyan.lean b/MockMockingbird/Smullyan.lean deleted file mode 100644 index e69de29..0000000 diff --git a/OneVariableCalculus.lean b/OneVariableCalculus.lean index f1f7109..8229284 100644 --- a/OneVariableCalculus.lean +++ b/OneVariableCalculus.lean @@ -1 +1,3 @@ -import OneVariableCalculus.Apostol \ No newline at end of file +import OneVariableCalculus.Chapters +import OneVariableCalculus.Exercises +import OneVariableCalculus.Real \ No newline at end of file diff --git a/OneVariableCalculus/Apostol.lean b/OneVariableCalculus/Apostol.lean deleted file mode 100644 index 595e783..0000000 --- a/OneVariableCalculus/Apostol.lean +++ /dev/null @@ -1,3 +0,0 @@ -import OneVariableCalculus.Apostol.Chapters -import OneVariableCalculus.Apostol.Exercises -import OneVariableCalculus.Apostol.Real \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Chapters.lean b/OneVariableCalculus/Apostol/Chapters.lean deleted file mode 100644 index 755a900..0000000 --- a/OneVariableCalculus/Apostol/Chapters.lean +++ /dev/null @@ -1 +0,0 @@ -import OneVariableCalculus.Apostol.Chapters.Chapter_I_3 \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Exercises.lean b/OneVariableCalculus/Apostol/Exercises.lean deleted file mode 100644 index d918be5..0000000 --- a/OneVariableCalculus/Apostol/Exercises.lean +++ /dev/null @@ -1 +0,0 @@ -import OneVariableCalculus.Apostol.Exercises.Exercises_I_3_12 \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Real.lean b/OneVariableCalculus/Apostol/Real.lean deleted file mode 100644 index 3dc33c5..0000000 --- a/OneVariableCalculus/Apostol/Real.lean +++ /dev/null @@ -1,3 +0,0 @@ -import OneVariableCalculus.Apostol.Real.Function -import OneVariableCalculus.Apostol.Real.Geometry -import OneVariableCalculus.Apostol.Real.Set \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Real/Function.lean b/OneVariableCalculus/Apostol/Real/Function.lean deleted file mode 100644 index fbf59d1..0000000 --- a/OneVariableCalculus/Apostol/Real/Function.lean +++ /dev/null @@ -1 +0,0 @@ -import OneVariableCalculus.Apostol.Real.Function.Step \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Real/Geometry.lean b/OneVariableCalculus/Apostol/Real/Geometry.lean deleted file mode 100644 index f93a06b..0000000 --- a/OneVariableCalculus/Apostol/Real/Geometry.lean +++ /dev/null @@ -1,3 +0,0 @@ -import OneVariableCalculus.Apostol.Real.Geometry.Area -import OneVariableCalculus.Apostol.Real.Geometry.Basic -import OneVariableCalculus.Apostol.Real.Geometry.Rectangle \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Real/Set.lean b/OneVariableCalculus/Apostol/Real/Set.lean deleted file mode 100644 index 1ae75b6..0000000 --- a/OneVariableCalculus/Apostol/Real/Set.lean +++ /dev/null @@ -1 +0,0 @@ -import OneVariableCalculus.Apostol.Real.Set.Partition \ No newline at end of file diff --git a/OneVariableCalculus/Chapters.lean b/OneVariableCalculus/Chapters.lean new file mode 100644 index 0000000..9a2293a --- /dev/null +++ b/OneVariableCalculus/Chapters.lean @@ -0,0 +1 @@ +import OneVariableCalculus.Chapters.Chapter_I_3 \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Chapters/Chapter_I_3.lean b/OneVariableCalculus/Chapters/Chapter_I_3.lean similarity index 100% rename from OneVariableCalculus/Apostol/Chapters/Chapter_I_3.lean rename to OneVariableCalculus/Chapters/Chapter_I_3.lean diff --git a/OneVariableCalculus/Apostol/Chapters/Chapter_I_3.tex b/OneVariableCalculus/Chapters/Chapter_I_3.tex similarity index 100% rename from OneVariableCalculus/Apostol/Chapters/Chapter_I_3.tex rename to OneVariableCalculus/Chapters/Chapter_I_3.tex diff --git a/OneVariableCalculus/Exercises.lean b/OneVariableCalculus/Exercises.lean new file mode 100644 index 0000000..2319674 --- /dev/null +++ b/OneVariableCalculus/Exercises.lean @@ -0,0 +1 @@ +import OneVariableCalculus.Exercises.Exercises_I_3_12 \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Exercises/Exercises_1_7.lean b/OneVariableCalculus/Exercises/Exercises_1_7.lean similarity index 100% rename from OneVariableCalculus/Apostol/Exercises/Exercises_1_7.lean rename to OneVariableCalculus/Exercises/Exercises_1_7.lean diff --git a/OneVariableCalculus/Apostol/Exercises/Exercises_I_3_12.lean b/OneVariableCalculus/Exercises/Exercises_I_3_12.lean similarity index 99% rename from OneVariableCalculus/Apostol/Exercises/Exercises_I_3_12.lean rename to OneVariableCalculus/Exercises/Exercises_I_3_12.lean index 1e0abe3..921f7fc 100644 --- a/OneVariableCalculus/Apostol/Exercises/Exercises_I_3_12.lean +++ b/OneVariableCalculus/Exercises/Exercises_I_3_12.lean @@ -10,7 +10,7 @@ import Mathlib.Data.Real.Sqrt import Mathlib.Tactic.LibrarySearch import Bookshelf.Real.Rational -import OneVariableCalculus.Apostol.Chapters.Chapter_I_3 +import OneVariableCalculus.Chapters.Chapter_I_3 -- ======================================== -- Exercise 1 diff --git a/OneVariableCalculus/Real.lean b/OneVariableCalculus/Real.lean new file mode 100644 index 0000000..47da635 --- /dev/null +++ b/OneVariableCalculus/Real.lean @@ -0,0 +1,3 @@ +import OneVariableCalculus.Real.Function +import OneVariableCalculus.Real.Geometry +import OneVariableCalculus.Real.Set \ No newline at end of file diff --git a/OneVariableCalculus/Real/Function.lean b/OneVariableCalculus/Real/Function.lean new file mode 100644 index 0000000..9680650 --- /dev/null +++ b/OneVariableCalculus/Real/Function.lean @@ -0,0 +1 @@ +import OneVariableCalculus.Real.Function.Step \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Real/Function/Step.lean b/OneVariableCalculus/Real/Function/Step.lean similarity index 92% rename from OneVariableCalculus/Apostol/Real/Function/Step.lean rename to OneVariableCalculus/Real/Function/Step.lean index 1076e3f..4f6d7a3 100644 --- a/OneVariableCalculus/Apostol/Real/Function/Step.lean +++ b/OneVariableCalculus/Real/Function/Step.lean @@ -2,7 +2,7 @@ import Mathlib.Data.Fin.Basic import Mathlib.Tactic.NormNum import Bookshelf.Real.Basic -import OneVariableCalculus.Apostol.Real.Set.Partition +import OneVariableCalculus.Real.Set.Partition namespace Real.Function diff --git a/OneVariableCalculus/Real/Geometry.lean b/OneVariableCalculus/Real/Geometry.lean new file mode 100644 index 0000000..157ca14 --- /dev/null +++ b/OneVariableCalculus/Real/Geometry.lean @@ -0,0 +1,3 @@ +import OneVariableCalculus.Real.Geometry.Area +import OneVariableCalculus.Real.Geometry.Basic +import OneVariableCalculus.Real.Geometry.Rectangle \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Real/Geometry/Area.lean b/OneVariableCalculus/Real/Geometry/Area.lean similarity index 97% rename from OneVariableCalculus/Apostol/Real/Geometry/Area.lean rename to OneVariableCalculus/Real/Geometry/Area.lean index 586f242..0286eeb 100644 --- a/OneVariableCalculus/Apostol/Real/Geometry/Area.lean +++ b/OneVariableCalculus/Real/Geometry/Area.lean @@ -3,8 +3,8 @@ Chapter 1.6 The concept of area as a set function -/ -import OneVariableCalculus.Apostol.Real.Function.Step -import OneVariableCalculus.Apostol.Real.Geometry.Rectangle +import OneVariableCalculus.Real.Function.Step +import OneVariableCalculus.Real.Geometry.Rectangle namespace Real.Geometry.Area diff --git a/OneVariableCalculus/Apostol/Real/Geometry/Basic.lean b/OneVariableCalculus/Real/Geometry/Basic.lean similarity index 100% rename from OneVariableCalculus/Apostol/Real/Geometry/Basic.lean rename to OneVariableCalculus/Real/Geometry/Basic.lean diff --git a/OneVariableCalculus/Apostol/Real/Geometry/Rectangle.lean b/OneVariableCalculus/Real/Geometry/Rectangle.lean similarity index 97% rename from OneVariableCalculus/Apostol/Real/Geometry/Rectangle.lean rename to OneVariableCalculus/Real/Geometry/Rectangle.lean index 00357ba..bd1f3bc 100644 --- a/OneVariableCalculus/Apostol/Real/Geometry/Rectangle.lean +++ b/OneVariableCalculus/Real/Geometry/Rectangle.lean @@ -1,4 +1,4 @@ -import OneVariableCalculus.Apostol.Real.Geometry.Basic +import OneVariableCalculus.Real.Geometry.Basic namespace Real diff --git a/OneVariableCalculus/Real/Set.lean b/OneVariableCalculus/Real/Set.lean new file mode 100644 index 0000000..286f6db --- /dev/null +++ b/OneVariableCalculus/Real/Set.lean @@ -0,0 +1 @@ +import OneVariableCalculus.Real.Set.Partition \ No newline at end of file diff --git a/OneVariableCalculus/Apostol/Real/Set/Partition.lean b/OneVariableCalculus/Real/Set/Partition.lean similarity index 100% rename from OneVariableCalculus/Apostol/Real/Set/Partition.lean rename to OneVariableCalculus/Real/Set/Partition.lean diff --git a/TheoremProvingInLean.lean b/TheoremProvingInLean.lean index 197a0a6..edb8563 100644 --- a/TheoremProvingInLean.lean +++ b/TheoremProvingInLean.lean @@ -1 +1,6 @@ -import TheoremProvingInLean.Avigad \ No newline at end of file +import TheoremProvingInLean.Chapter2 +import TheoremProvingInLean.Chapter3 +import TheoremProvingInLean.Chapter4 +import TheoremProvingInLean.Chapter5 +import TheoremProvingInLean.Chapter7 +import TheoremProvingInLean.Chapter8 diff --git a/TheoremProvingInLean/Avigad.lean b/TheoremProvingInLean/Avigad.lean deleted file mode 100644 index 7b091f1..0000000 --- a/TheoremProvingInLean/Avigad.lean +++ /dev/null @@ -1,6 +0,0 @@ -import TheoremProvingInLean.Avigad.Chapter2 -import TheoremProvingInLean.Avigad.Chapter3 -import TheoremProvingInLean.Avigad.Chapter4 -import TheoremProvingInLean.Avigad.Chapter5 -import TheoremProvingInLean.Avigad.Chapter7 -import TheoremProvingInLean.Avigad.Chapter8 diff --git a/TheoremProvingInLean/Avigad/Chapter2.lean b/TheoremProvingInLean/Chapter2.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter2.lean rename to TheoremProvingInLean/Chapter2.lean diff --git a/TheoremProvingInLean/Avigad/Chapter3.lean b/TheoremProvingInLean/Chapter3.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter3.lean rename to TheoremProvingInLean/Chapter3.lean diff --git a/TheoremProvingInLean/Avigad/Chapter4.lean b/TheoremProvingInLean/Chapter4.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter4.lean rename to TheoremProvingInLean/Chapter4.lean diff --git a/TheoremProvingInLean/Avigad/Chapter5.lean b/TheoremProvingInLean/Chapter5.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter5.lean rename to TheoremProvingInLean/Chapter5.lean diff --git a/TheoremProvingInLean/Avigad/Chapter7.lean b/TheoremProvingInLean/Chapter7.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter7.lean rename to TheoremProvingInLean/Chapter7.lean diff --git a/TheoremProvingInLean/Avigad/Chapter8.lean b/TheoremProvingInLean/Chapter8.lean similarity index 100% rename from TheoremProvingInLean/Avigad/Chapter8.lean rename to TheoremProvingInLean/Chapter8.lean