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