diff --git a/Bookshelf/Apostol/Chapter_1_07.tex b/Bookshelf/Apostol/Chapter_1_07.tex index 53555f5..7c81b52 100644 --- a/Bookshelf/Apostol/Chapter_1_07.tex +++ b/Bookshelf/Apostol/Chapter_1_07.tex @@ -6,8 +6,9 @@ \graphicspath{{./images/}} -\newcommand{\larea}[2]{\lean{../..}{Common/Real/Geometry/Area}{#1}{#2}} -\newcommand{\lrect}[2]{\lean{../..}{Common/Real/Geometry/Rectangle}{#1}{#2}} +\externaldocument[A:] + {../../Common/Real/Geometry/Area} + [../../Common/Real/Geometry/Area.pdf] \begin{document} @@ -29,10 +30,9 @@ A set consisting of a single point. \begin{proof} Let $S$ be a set consisting of a single point. - By definition of a \lrect{Real.Point}{Point}, $S$ is a rectangle in which all - vertices coincide. - By \larea{Choice-of-Scale}{Choice of Scale}, $S$ is measurable with area its - width times its height. + 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 + its height. The width and height of $S$ is trivially zero. Therefore $a(S) = (0)(0) = 0$. @@ -65,7 +65,7 @@ A set consisting of a finite number of points in a plane. By construction, $S_{k+1} = S_k \cup T$. By the induction hypothesis, $S_k$ is measurable with area $0$. By \nameref{sub:exercise-1a}, $T$ is measurable with area $0$. - By the \larea{Additive-Property}{Additive Property}, $S_k \cup T$ is + By the \nameref{A:sec:additive-property}, $S_k \cup T$ is measurable, $S_k \cap T$ is measurable, and \begin{align} a(S_{k+1}) @@ -111,10 +111,10 @@ The union of a finite collection of line segments in a plane. \paragraph{Base Case}% Consider a set $S$ consisting of a single line segment in a plane. - By definition of a \lrect{Real.LineSemgnet}{Line Segment}, $S$ is a - rectangle in which one side has dimension $0$. - By \larea{Choice-of-Scale}{Choice of Scale}, $S$ is measurable with area its - width $w$ times its height $h$. + By definition of a Line Segment, $S$ is a rectangle in which one side has + dimension $0$. + By \nameref{A:sec:choice-scale}, $S$ is measurable with area its width $w$ + times its height $h$. Therefore $a(S) = wh = 0$. Thus $P(1)$ holds. @@ -128,8 +128,8 @@ The union of a finite collection of line segments in a plane. By construction, $S_{k+1} = S_k \cup T$. By the induction hypothesis, $S_k$ is measurable with area $0$. By the base case, $T$ is measurable with area $0$. - By the \larea{Additive-Property}{Additive Property}, $S_k \cup T$ is - measurable, $S_k \cap T$ is measurable, and + By the \nameref{A:sec:additive-property}, $S_k \cup T$ is measurable, + $S_k \cap T$ is measurable, and \begin{align} a(S_{k+1}) & = a(S_k \cup T) \nonumber \\ @@ -190,10 +190,10 @@ Prove that every triangular region is measurable and that its area is one half \centering \end{figure} - By \larea{Choice-of-Scale}{Choice of Scale}, both $R$ and $S$ are measurable. + By \nameref{A:sec:choice-scale}, both $R$ and $S$ are measurable. By this same axiom, $a(R) = ab$ and $a(S) = ca\sin{\theta}$. - By the \larea{Additive-Property}{Additive Property}, $R \cup S$ and $R \cap S$ - are both measurable. + By the \nameref{A:sec:additive-property}, $R \cup S$ and $R \cap S$ are both + measurable. $a(R \cap S) = a(T)$ and $a(R \cup S)$ can be determined by noting that $R$'s construction implies identity $a(R) = 2a(T)$. Therefore @@ -206,8 +206,8 @@ Prove that every triangular region is measurable and that its area is one half & = ab + ca\sin{\theta} - ca\sin{\theta} - a(T). \end{align*} Solving for $a(T)$ gives the desired identity: $$a(T) = \frac{1}{2}ab.$$ - By \larea{Invariance-Under-Congruence}{Invariance Under Congruence}, - $a(T') = a(T)$, concluding our proof. + By \nameref{A:sec:invariance-under-congruence}, $a(T') = a(T)$, concluding our + proof. \end{proof} @@ -233,10 +233,10 @@ Prove that every trapezoid and every parallelogram is measurable and derive the Suppose $S$ is a right trapezoid. Then $S$ is the union of non-overlapping rectangle $R$ of width $b_1$ and height $h$ with right triangle $T$ of base $b_2 - b_1$ and height $h$. - By \larea{Choice-of-Scale}{Choice of Scale}, $R$ is measurable. + By \nameref{A:sec:choice-scale}, $R$ is measurable. By \nameref{sec:exercise-2}, $T$ is measurable. - By the \larea{Additive-Property}{Additive Property}, $R \cup T$ and $R \cap T$ - are both measurable and + By the \nameref{A:sec:additive-property}, $R \cup T$ and $R \cap T$ are both + measurable and \begin{align*} a(S) & = a(R \cup T) \\ @@ -256,8 +256,8 @@ Prove that every trapezoid and every parallelogram is measurable and derive the Then $R$ has longer base edge of length $b_2 - c$. By \nameref{sec:exercise-2}, $T$ is measurable. By Case 1, $R$ is measurable. - By the \larea{Additive-Property}{Additive Property}, $R \cup T$ and $R \cap T$ - are both measurable and + By the \nameref{A:sec:additive-property}, $R \cup T$ and $R \cap T$ are both + measurable and \begin{align*} a(S) & = a(T) + a(R) - a(R \cap T) \\ @@ -274,7 +274,7 @@ Prove that every trapezoid and every parallelogram is measurable and derive the Let $c$ denote the length of base $T$. Reflect $T$ vertically to form another right triangle, say $T'$. Then $T' \cup R$ is an acute trapezoid. - By \larea{Invariance-Under-Congruence}{Invariance Under Congruence}, + By \nameref{A:sec:invariance-under-congruence}, \begin{equation} \label{par:exercise-3-case-3-eq1} \tag{3.1} @@ -301,7 +301,7 @@ Prove that every trapezoid and every parallelogram is measurable and derive the Let $c$ denote the length of base $T$. Reflect $T$ vertically to form another right triangle, say $T'$. Then $T' \cup R$ is an acute trapezoid. - By \larea{Invariance-Under-Congruence}{Invariance Under Congruence}, + By \nameref{A:sec:invariance-under-congruence}, \begin{equation} \label{par:exercise-3-eq2} \tag{3.2} @@ -338,8 +338,7 @@ Prove that the formula is valid for rectangles with sides parallel to the We assume $P$ has three non-collinear points, ruling out any instances of points or line segments. - By \larea{Choice-of-Scale}{Choice of Scale}, $P$ is measurable with area - $a(P) = wh$. + By \nameref{A:sec:choice-scale}, $P$ is measurable with area $a(P) = wh$. By construction, $P$ has $I = (w - 1)(h - 1)$ interior lattice points and $B = 2(w + h)$ lattice points on its boundary. The following shows the lattice point area formula is in agreement with @@ -456,8 +455,8 @@ Use induction on the number of edges to construct a proof for general polygons. & = a(S) + (I_T + \frac{1}{2}B_T - 1) & \text{induction hypothesis} \\ & = a(S) + a(T). & \text{base case} \end{align*} - By the \larea{Additive-Property}{Additive Property}, $S \cup T$ is - measurable, $S \cap T$ is measurable, and + By the \nameref{A:sec:additive-property}, $S \cup T$ is measurable, + $S \cap T$ is measurable, and \begin{align*} a(P) & = a(S \cup T) \\ diff --git a/Bookshelf/Apostol/Chapter_1_11.tex b/Bookshelf/Apostol/Chapter_1_11.tex index 61b5c70..09325f6 100644 --- a/Bookshelf/Apostol/Chapter_1_11.tex +++ b/Bookshelf/Apostol/Chapter_1_11.tex @@ -2,11 +2,9 @@ \input{../../preamble} -\newcommand{\link}[1]{\lean{../..} - {Bookshelf/Apostol/Chapter\_1\_11} % Location - {Apostol.Chapter\_1\_11.#1} % Fragment - {Chapter\_1\_11.#1} % Presentation -} +\newcommand{\lean}[1]{\href + {./Chapter\_1\_11.html\#Apostol.Chapter\_1\_11.#1} + {Apostol.Chapter\_1\_11.#1}} \begin{document} @@ -24,7 +22,7 @@ $\floor{x + n} = \floor{x} + n$ for every integer $n$. \begin{proof} - \link{exercise\_4a} + \lean{exercise\_4a} \end{proof} @@ -42,8 +40,8 @@ $\floor{-x} = \ % Force space prior to *Proof.* \begin{enumerate}[(a)] - \item \link{exercise\_4b\_1} - \item \link{exercise\_4b\_2} + \item \lean{exercise\_4b\_1} + \item \lean{exercise\_4b\_2} \end{enumerate} \end{proof} @@ -55,7 +53,7 @@ $\floor{x + y} = \floor{x} + \floor{y}$ or $\floor{x} + \floor{y} + 1$. \begin{proof} - \link{exercise\_4c} + \lean{exercise\_4c} \end{proof} @@ -66,7 +64,7 @@ $\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$ \begin{proof} - \link{exercise\_4d} + \lean{exercise\_4d} \end{proof} @@ -77,7 +75,7 @@ $\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$ \begin{proof} - \link{exercise\_4e} + \lean{exercise\_4e} \end{proof} @@ -92,7 +90,7 @@ State and prove such a generalization. \begin{proof} - \link{exercise\_5} + \lean{exercise\_5} \divider @@ -223,7 +221,7 @@ Now apply Exercises 4(a) and (b) to the bracket on the right. \begin{proof} - \link{exercise\_7b} + \lean{exercise\_7b} \end{proof} diff --git a/Bookshelf/Apostol/Chapter_I_03.tex b/Bookshelf/Apostol/Chapter_I_03.tex index 2cb5c0c..695b893 100644 --- a/Bookshelf/Apostol/Chapter_I_03.tex +++ b/Bookshelf/Apostol/Chapter_I_03.tex @@ -2,11 +2,9 @@ \input{../../preamble} -\newcommand{\link}[1]{\lean{../..} - {Bookshelf/Apostol/Chapter\_I\_03} % Location - {Apostol.Chapter\_I\_03.#1} % Fragment - {Chapter\_I\_03.#1} % Presentation -} +\newcommand{\lean}[1]{\href + {./Chapter\_I\_03.html\#Apostol.Chapter\_I\_03.#1} + {Apostol.Chapter\_I\_03.#1}} \begin{document} @@ -19,7 +17,7 @@ Nonempty set $S$ has supremum $L$ if and only if set $-S$ has infimum $-L$. \begin{proof} - \link{is\_lub\_neg\_set\_iff\_is\_glb\_set\_neg} + \lean{is\_lub\_neg\_set\_iff\_is\_glb\_set\_neg} \divider @@ -40,7 +38,7 @@ Every nonempty set $S$ that is bounded below has a greatest lower bound; that \begin{proof} - \link{exists\_isGLB} + \lean{exists\_isGLB} \divider @@ -59,7 +57,7 @@ For every real $x$ there exists a positive integer $n$ such that $n > x$. \begin{proof} - \link{exists\_pnat\_geq\_self} + \lean{exists\_pnat\_geq\_self} \divider @@ -82,7 +80,7 @@ If $x > 0$ and if $y$ is an arbitrary real number, there exists a positive \begin{proof} - \link{exists\_pnat\_mul\_self\_geq\_of\_pos} + \lean{exists\_pnat\_mul\_self\_geq\_of\_pos} \divider @@ -101,7 +99,7 @@ If three real numbers $a$, $x$, and $y$ satisfy the inequalities \begin{proof} - \link{forall\_pnat\_leq\_self\_leq\_frac\_imp\_eq} + \lean{forall\_pnat\_leq\_self\_leq\_frac\_imp\_eq} \divider @@ -144,7 +142,7 @@ If three real numbers $a$, $x$, and $y$ satisfy the inequalities \begin{proof} - \link{forall\_pnat\_frac\_leq\_self\_leq\_imp\_eq} + \lean{forall\_pnat\_frac\_leq\_self\_leq\_imp\_eq} \divider @@ -191,7 +189,7 @@ If $S$ has a supremum, then for some $x$ in $S$ we have $x > \sup{S} - h$. \begin{proof} - \link{sup\_imp\_exists\_gt\_sup\_sub\_delta} + \lean{sup\_imp\_exists\_gt\_sup\_sub\_delta} \divider @@ -213,7 +211,7 @@ If $S$ has an infimum, then for some $x$ in $S$ we have $x < \inf{S} + h$. \begin{proof} - \link{inf\_imp\_exists\_lt\_inf\_add\_delta} + \lean{inf\_imp\_exists\_lt\_inf\_add\_delta} \divider @@ -244,7 +242,7 @@ If each of $A$ and $B$ has a supremum, then $C$ has a supremum, and \begin{proof} - \link{sup\_minkowski\_sum\_eq\_sup\_add\_sup} + \lean{sup\_minkowski\_sum\_eq\_sup\_add\_sup} \divider @@ -312,7 +310,7 @@ If each of $A$ and $B$ has an infimum, then $C$ has an infimum, and \begin{proof} - \link{inf\_minkowski\_sum\_eq\_inf\_add\_inf} + \lean{inf\_minkowski\_sum\_eq\_inf\_add\_inf} \divider @@ -381,7 +379,7 @@ Given two nonempty subsets $S$ and $T$ of $\mathbb{R}$ such that $$s \leq t$$ \begin{proof} - \link{forall\_mem\_le\_forall\_mem\_imp\_sup\_le\_inf} + \lean{forall\_mem\_le\_forall\_mem\_imp\_sup\_le\_inf} \divider diff --git a/Bookshelf/Enderton/Chapter_0.tex b/Bookshelf/Enderton/Chapter_0.tex index 5d04a36..4500a54 100644 --- a/Bookshelf/Enderton/Chapter_0.tex +++ b/Bookshelf/Enderton/Chapter_0.tex @@ -2,11 +2,9 @@ \input{../../preamble} -\newcommand{\link}[1]{\lean{../..} - {Bookshelf/Enderton/Chapter\_0} % Location - {Enderton.Chapter\_0.#1} % Fragment - {Chapter\_0.#1} % Presentation -} +\newcommand{\lean}[1]{\href + {./Chapter\_0.html\#Enderton.Chapter\_0.#1} + {Enderton.Chapter\_0.#1}} \begin{document} @@ -21,7 +19,7 @@ Then $x_1 = \langle y_1, \ldots, y_{k+1} \rangle$. \begin{proof} - \link{lemma\_0a} + \lean{lemma\_0a} \end{proof} diff --git a/Common/Real/Geometry/Area.tex b/Common/Real/Geometry/Area.tex index 4b825b9..b58d338 100644 --- a/Common/Real/Geometry/Area.tex +++ b/Common/Real/Geometry/Area.tex @@ -1,12 +1,8 @@ \documentclass{article} -\input{../../preamble} +\input{../../../preamble} -\newcommand{\link}[2]{\lean{../..} - {Common/Real/Geometry/Area} % Location - {#1} % Fragment - {#2} % Presentation -} +\newcommand{\lean}[2]{\href{./Area.html\##1}{#2}} \begin{document} @@ -23,7 +19,7 @@ For each set $S$ in $\mathscr{M}$, we have $a(S) \geq 0$. \begin{axiom} - \link{Nonnegative-Property}{Nonnegative Property} + \lean{Nonnegative-Property}{Nonnegative Property} \end{axiom} @@ -35,7 +31,7 @@ If $S$ and $T$ are in $\mathscr{M}$, then $S \cup T$ and $S \cap T$ are in \begin{axiom} - \link{Additive-Property}{Additive Property} + \lean{Additive-Property}{Additive Property} \end{axiom} @@ -47,7 +43,7 @@ If $S$ and $T$ are in $\mathscr{M}$ with $S \subseteq T$, then $T - S$ is in \begin{axiom} - \link{Difference-Property}{Difference Property} + \lean{Difference-Property}{Difference Property} \end{axiom} @@ -59,7 +55,7 @@ If a set $S$ is in $\mathscr{M}$ and if $T$ is congruent to $S$, then $T$ is \begin{axiom} - \link{Invariant-Under-Congruence}{Invariance Under Congruence} + \lean{Invariant-Under-Congruence}{Invariance Under Congruence} \end{axiom} @@ -71,7 +67,7 @@ If the edges of $R$ have lengths $h$ and $k$, then $a(R) = hk$. \begin{axiom} - \link{Choice-of-Scale}{Choice of Scale} + \lean{Choice-of-Scale}{Choice of Scale} \end{axiom} @@ -90,7 +86,7 @@ If there is one and only one number $c$ which satisfies the inequalities \begin{axiom} - \link{Exhaustion-Property}{Exhaustion Property} + \lean{Exhaustion-Property}{Exhaustion Property} \end{axiom} diff --git a/Common/Real/Sequence/Arithmetic.tex b/Common/Real/Sequence/Arithmetic.tex index dacffd7..12389c6 100644 --- a/Common/Real/Sequence/Arithmetic.tex +++ b/Common/Real/Sequence/Arithmetic.tex @@ -2,11 +2,9 @@ \input{../../../preamble} -\newcommand{\link}[1]{\lean{../../..} - {Common/Real/Sequence/Arithmetic} % Location - {Real.Arithmetic.#1} % Fragment - {Real.Arithmetic.#1} % Presentation -} +\newcommand{\lean}[1]{\href + {./Arithmetic.html\#Real.Arithmetic.#1} + {Real.Arithmetic.#1}} \begin{document} @@ -19,7 +17,7 @@ $$\sum_{i=0}^n a_i = \frac{(n + 1)(a_0 + a_n)}{2}.$$ \begin{proof} - \link{sum\_recursive\_closed} + \lean{sum\_recursive\_closed} \end{proof} diff --git a/Common/Real/Sequence/Geometric.tex b/Common/Real/Sequence/Geometric.tex index ac23235..0df893f 100644 --- a/Common/Real/Sequence/Geometric.tex +++ b/Common/Real/Sequence/Geometric.tex @@ -2,11 +2,9 @@ \input{../../../preamble} -\newcommand{\link}[1]{\lean{../../..} - {Common/Real/Sequence/Geometric} % Location - {Real.Geometric.#1} % Fragment - {Real.Geometric.#1} % Presentation -} +\newcommand{\lean}[1]{\href + {./Geometric.html\#Real.Geometric.#1} + {Real.Geometric.#1}} \begin{document} @@ -19,7 +17,7 @@ $$\sum_{i=0}^n a_i = \frac{a_0(1 - r^{n+1})}{1 - r}.$$ \begin{proof} - \link{sum\_recursive\_closed} + \lean{sum\_recursive\_closed} \end{proof} diff --git a/README.md b/README.md index 02c15a8..be6ba94 100644 --- a/README.md +++ b/README.md @@ -30,11 +30,10 @@ project. A color/symbol code is used on generated PDF headers to indicate their status: -* Teal coloring (with a checkmark) indicates the corresponding proof is - complete. That is, the proof has been written in TeX and also formally - verified in Lean. -* Magenta coloring (with a spinner) indicates the corresponding proof is in - progress. That is, a proof in both TeX and Lean have not yet been finished, - but is actively being worked on. -* Red coloring (with a warning) indicates the formal Lean proof has not yet been - started. It may or may not also indicate the TeX proof has been written. +* Teal coloring indicates the corresponding proof is complete. That is, the + proof has been written in TeX and also formally verified in Lean. +* Magenta coloring indicates the corresponding proof is in progress. That is, a + proof in both TeX and Lean have not yet been finished, but is actively being + worked on. +* Red coloring indicates the formal Lean proof has not yet been started. It may + or may not also indicate the TeX proof has been written. diff --git a/lake-manifest.json b/lake-manifest.json index b5e122a..a9a3aa1 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": "80a4dc8d508161c859dbbb455f3855e051a28890", + "rev": "3f941dc8a814321498082da49f4a8430bbfbbb6c", "name": "doc-gen4", - "inputRev?": "80a4dc8d508161c859dbbb455f3855e051a28890"}}, + "inputRev?": "3f941dc8a814321498082da49f4a8430bbfbbb6c"}}, {"git": {"url": "https://github.com/mhuisi/lean4-cli", "subDir?": null, diff --git a/lakefile.lean b/lakefile.lean index fd5969f..9524f10 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" @ - "80a4dc8d508161c859dbbb455f3855e051a28890" + "3f941dc8a814321498082da49f4a8430bbfbbb6c" @[default_target] lean_lib «Bookshelf» { diff --git a/preamble.tex b/preamble.tex index 49d6b05..93f11c7 100644 --- a/preamble.tex +++ b/preamble.tex @@ -3,23 +3,18 @@ \usepackage{environ} \usepackage{fancybox} \usepackage{fontawesome5} -\usepackage{hyperref} \usepackage{mathrsfs} -\usepackage{soul, xcolor} +\usepackage{soul} +\usepackage{xcolor} +% `hyperref` comes after `xr-hyper`. +\usepackage{xr-hyper} +\usepackage{hyperref} % ======================================== % Linking % ======================================== \hypersetup{colorlinks=true, urlcolor=blue} - -% The first argument refers to a relative path upward from a current file to -% the root of the workspace (i.e. where this `preamble.tex` file is located). -% #1 - Path to root -% #2 - Location -% #3 - Fragment -% #4 - Presentation -\newcommand{\lean}[4]{\href{#1/#2.html\##3}{#4}} \newcommand{\hyperlabel}[1]{% \label{#1}% \hypertarget{#1}{}} @@ -56,7 +51,7 @@ \DeclareRobustCommand{\verified}[1]{% \texorpdfstring{\color{teal}#1\ \faCheckCircle}{#1}} \DeclareRobustCommand{\proceeding}[1]{% - \texorpdfstring{\color{magenta}#1\ \faSpinner}{#1}} + \texorpdfstring{\color{magenta}#1\ \faDotCircle[regular]}{#1}} \DeclareRobustCommand{\unverified}[1]{% \texorpdfstring{\color{red}#1\ \faExclamationCircle}{#1}}