diff --git a/Bookshelf/Real/Sequence/Arithmetic_tex.tex b/Bookshelf/Real/Sequence/Arithmetic.tex similarity index 94% rename from Bookshelf/Real/Sequence/Arithmetic_tex.tex rename to Bookshelf/Real/Sequence/Arithmetic.tex index 318d299..e415bd3 100644 --- a/Bookshelf/Real/Sequence/Arithmetic_tex.tex +++ b/Bookshelf/Real/Sequence/Arithmetic.tex @@ -1,6 +1,6 @@ \documentclass{article} -\input{preamble} +\input{../../../preamble} \newcommand{\link}[1]{\lean{../../..} {Bookshelf/Real/Sequence/Arithmetic} diff --git a/Bookshelf/Real/Sequence/Geometric_tex.tex b/Bookshelf/Real/Sequence/Geometric.tex similarity index 94% rename from Bookshelf/Real/Sequence/Geometric_tex.tex rename to Bookshelf/Real/Sequence/Geometric.tex index 971177a..af35fc5 100644 --- a/Bookshelf/Real/Sequence/Geometric_tex.tex +++ b/Bookshelf/Real/Sequence/Geometric.tex @@ -1,6 +1,6 @@ \documentclass{article} -\input{preamble} +\input{../../../preamble} \newcommand{\link}[1]{\lean{../../..} {Bookshelf/Real/Sequence/Geometric} diff --git a/Exercises/Apostol/Chapter_I_3_tex.tex b/Exercises/Apostol/Chapter_I_3.tex similarity index 96% rename from Exercises/Apostol/Chapter_I_3_tex.tex rename to Exercises/Apostol/Chapter_I_3.tex index 865a84b..1368235 100644 --- a/Exercises/Apostol/Chapter_I_3_tex.tex +++ b/Exercises/Apostol/Chapter_I_3.tex @@ -1,7 +1,7 @@ \documentclass{article} \usepackage[shortlabels]{enumitem} -\input{preamble} +\input{../../preamble} \newcommand{\link}[1]{\lean{../..} {Exercises/Apostol/Chapter\_I\_3} @@ -72,6 +72,8 @@ Let $h$ be a given positive number and let $S$ be a set of real numbers. \begin{proof} + \ % Force space prior to *Proof.* + \begin{enumerate}[(a)] \item \link{sup\_imp\_exists\_gt\_sup\_sub\_delta} \item \link{inf\_imp\_exists\_lt\_inf\_add\_delta} @@ -94,6 +96,8 @@ $$C = \{a + b : a \in A, b \in B\}.$$ \begin{proof} + \ % Force space prior to *Proof.* + \begin{enumerate}[(a)] \item \link{sup\_minkowski\_sum\_eq\_sup\_add\_sup} \item \link{inf\_minkowski\_sum\_eq\_inf\_add\_inf} diff --git a/Exercises/Apostol/Exercises_1_7_tex.tex b/Exercises/Apostol/Exercises_1_7.tex similarity index 99% rename from Exercises/Apostol/Exercises_1_7_tex.tex rename to Exercises/Apostol/Exercises_1_7.tex index 7a50d3d..51268f3 100644 --- a/Exercises/Apostol/Exercises_1_7_tex.tex +++ b/Exercises/Apostol/Exercises_1_7.tex @@ -1,7 +1,7 @@ \documentclass{article} \usepackage{amsmath} -\input{preamble} +\input{../../preamble} \newcommand{\larea}[2]{\lean{../..}{Bookshelf/Real/Geometry/Area}{#1}{#2}} \newcommand{\lrect}[2]{\lean{../..}{Bookshelf/Real/Geometry/Rectangle}{#1}{#2}} diff --git a/Exercises/Enderton/Chapter0_tex.tex b/Exercises/Enderton/Chapter0.tex similarity index 94% rename from Exercises/Enderton/Chapter0_tex.tex rename to Exercises/Enderton/Chapter0.tex index 916c711..c2817c6 100644 --- a/Exercises/Enderton/Chapter0_tex.tex +++ b/Exercises/Enderton/Chapter0.tex @@ -1,6 +1,6 @@ \documentclass{article} -\input{preamble} +\input{../../preamble} \newcommand{\link}[1]{\lean{../..} {Exercises/Enderton/Chapter0} diff --git a/lake-manifest.json b/lake-manifest.json index 3c67506..2339754 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -16,9 +16,9 @@ {"git": {"url": "https://github.com/jrpotter/bookshelf-docgen.git", "subDir?": null, - "rev": "b083d636c2581e72da9d18023240319dd5eca43a", + "rev": "dee1ea599fd459db8f40201a32338c606b1944e8", "name": "doc-gen4", - "inputRev?": "b083d636c2581e72da9d18023240319dd5eca43a"}}, + "inputRev?": "dee1ea599fd459db8f40201a32338c606b1944e8"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 35c3bbc..9a02604 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -12,7 +12,7 @@ require std4 from git "6006307d2ceb8743fea7e00ba0036af8654d0347" require «doc-gen4» from git "https://github.com/jrpotter/bookshelf-docgen.git" @ - "b083d636c2581e72da9d18023240319dd5eca43a" + "dee1ea599fd459db8f40201a32338c606b1944e8" @[default_target] lean_lib «Bookshelf» {