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