diff --git a/Bookshelf/Apostol/Chapter_1_07.tex b/Bookshelf/Apostol/Chapter_1_07.tex index 7c81b52..d265578 100644 --- a/Bookshelf/Apostol/Chapter_1_07.tex +++ b/Bookshelf/Apostol/Chapter_1_07.tex @@ -31,7 +31,7 @@ A set consisting of a single point. Let $S$ be a set consisting of a single point. By definition of a Point, $S$ is a rectangle in which all vertices coincide. - By \nameref{A:sec:choice-scale} $S$ is measurable with area its width times + By \nameref{A:sec:choice-scale}, $S$ is measurable with area its width times its height. The width and height of $S$ is trivially zero. Therefore $a(S) = (0)(0) = 0$. diff --git a/lake-manifest.json b/lake-manifest.json index a9a3aa1..94d4ece 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": "3f941dc8a814321498082da49f4a8430bbfbbb6c", + "rev": "87ecc512444afd073a2b201ef25caf3ef5fc74b1", "name": "doc-gen4", - "inputRev?": "3f941dc8a814321498082da49f4a8430bbfbbb6c"}}, + "inputRev?": "87ecc512444afd073a2b201ef25caf3ef5fc74b1"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index 9524f10..1ed3b44 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" @ - "3f941dc8a814321498082da49f4a8430bbfbbb6c" + "87ecc512444afd073a2b201ef25caf3ef5fc74b1" @[default_target] lean_lib «Bookshelf» { diff --git a/preamble.tex b/preamble.tex index 93f11c7..502fc5b 100644 --- a/preamble.tex +++ b/preamble.tex @@ -49,11 +49,11 @@ % and a corresponding Lean proof has been written. If a Lean proof is in % progress, it's in a "proceeding" state. Otherwise it is unverified. \DeclareRobustCommand{\verified}[1]{% - \texorpdfstring{\color{teal}#1\ \faCheckCircle}{#1}} + \texorpdfstring{\color{teal}\faCheckCircle\ #1}{#1}} \DeclareRobustCommand{\proceeding}[1]{% - \texorpdfstring{\color{magenta}#1\ \faDotCircle[regular]}{#1}} + \texorpdfstring{\color{magenta}\faDotCircle[regular]\ #1}{#1}} \DeclareRobustCommand{\unverified}[1]{% - \texorpdfstring{\color{red}#1\ \faExclamationCircle}{#1}} + \texorpdfstring{\color{red}\faExclamationCircle\ #1}{#1}} % ======================================== % Math