diff --git a/Bookshelf/Apostol.tex b/Bookshelf/Apostol.tex
index e04e2cc..201c23f 100644
--- a/Bookshelf/Apostol.tex
+++ b/Bookshelf/Apostol.tex
@@ -36,6 +36,18 @@ The \textbf{characteristic function} of $S$ is the function $\mathcal{X}_S$ such
\end{definition}
+\section{\defined{Completeness Axiom}}%
+\label{ref:completeness-axiom}
+
+Every nonempty set $S$ of real numbers which is bounded above has a supremum;
+ that is, there is a real number $B$ such that $B = \sup{S}$.
+
+\begin{axiom}
+
+ \lean*{Mathlib/Data/Real/Basic}{Real.exists\_isLUB}
+
+\end{axiom}
+
\section{\defined{Infimum}}%
\label{ref:infimum}
@@ -53,7 +65,7 @@ Such a number $B$ is also known as the \textbf{greatest lower bound}.
\end{definition}
-\section{\partial{Integrable}}%
+\section{\pending{Integrable}}%
\label{ref:integrable}
Let $f$ be a function defined and bounded on $[a, b]$.
@@ -62,7 +74,7 @@ $f$ is said to be \textbf{integrable} if there exists one and only one number
If $f$ is integrable on $[a, b]$, we say that the integral
$\int_a^b f(x) \mathop{dx}$ \textbf{exists}.
-\section{\partial{Integral of a Bounded Function}}%
+\section{\pending{Integral of a Bounded Function}}%
\label{ref:integral-bounded-function}
Let $f$ be a function defined and bounded on $[a, b]$.
@@ -90,7 +102,7 @@ The function $f$ is called the \textbf{integrand}, the numbers $a$ and $b$ are
called the \textbf{limits of integration}, and the interval $[a, b]$ the
\textbf{interval of integration}.
-\section{\partial{Integral of a Step Function}}%
+\section{\pending{Integral of a Step Function}}%
\label{ref:integral-step-function}
Let $s$ be a \nameref{ref:step-function} defined on $[a, b]$, and let
@@ -106,7 +118,7 @@ The \textbf{integral of $s$ from $a$ to $b$}, denoted by the symbol
If $a < b$, we define $\int_b^a s(x) \mathop{dx} = -\int_a^b s(x) \mathop{dx}$.
We also define $\int_a^a s(x) \mathop{dx} = 0$.
-\section{\partial{Lower Integral}}%
+\section{\pending{Lower Integral}}%
\label{ref:lower-integral}
Let $f$ be a function bounded on $[a, b]$ and $S$ denote the set of numbers
@@ -116,7 +128,7 @@ That is, let $$S = \left\{ \int_a^b s(x) \mathop{dx} : s \leq f \right\}.$$
The number $\sup{S}$ is called the \textbf{lower integral of $f$}.
It is denoted as $\ubar{I}(f)$.
-\section{\partial{Monotonic}}%
+\section{\pending{Monotonic}}%
\label{ref:monotonic}
A function $f$ is called \textbf{monotonic} on set $S$ if it is increasing on
@@ -152,7 +164,7 @@ A collection of points satisfying \eqref{sec:partition-eq1} is called a
\end{definition}
-\section{\partial{Refinement}}%
+\section{\pending{Refinement}}%
\label{ref:refinement}
Let $P$ be a \nameref{ref:partition} of closed interval $[a, b]$.
@@ -199,7 +211,7 @@ Such a number $B$ is also known as the \textbf{least upper bound}.
\end{definition}
-\section{\partial{Upper Integral}}%
+\section{\pending{Upper Integral}}%
\label{ref:upper-integral}
Let $f$ be a function bounded on $[a, b]$ and $T$ denote the set of numbers
@@ -214,18 +226,6 @@ It is denoted as $\bar{I}(f)$.
\chapter{A Set of Axioms for the Real-Number System}%
\label{chap:set-axioms-real-number-system}
-\section{\defined{Completeness Axiom}}%
-\label{sec:completeness-axiom}
-
-Every nonempty set $S$ of real numbers which is bounded above has a supremum;
- that is, there is a real number $B$ such that $B = \sup{S}$.
-
-\begin{axiom}
-
- \lean*{Mathlib/Data/Real/Basic}{Real.exists\_isLUB}
-
-\end{axiom}
-
\section{\verified{Lemma 1}}%
\label{sec:lemma-1}
@@ -267,7 +267,7 @@ Every nonempty set $S$ of real numbers which is bounded above has a supremum;
Let $S$ be a nonempty set bounded below by $x$.
Then $-S$ is nonempty and bounded above by $x$.
- By the \nameref{sec:completeness-axiom}, there exists a
+ By the \nameref{ref:completeness-axiom}, there exists a
\nameref{ref:supremum} $L$ of $-S$.
By \nameref{sec:lemma-1}, $L$ is a supremum of $-S$ if and only if $-L$ is an
infimum of $S$.
@@ -731,7 +731,7 @@ If the edges of $R$ have lengths $h$ and $k$, then $a(R) = hk$.
\end{axiom}
-\subsection{\partial{Exhaustion Property}}%
+\subsection{\pending{Exhaustion Property}}%
\label{sub:area-exhaustion-property}
Let $Q$ be a set that can be enclosed between two step regions $S$ and $T$, so
@@ -754,12 +754,12 @@ If there is one and only one number $c$ which satisfies the inequalities
\section{Exercises 1.7}%
\label{sec:exercises-1.7}
-\subsection{\partial{Exercise 1.7.1}}%
+\subsection{\pending{Exercise 1.7.1}}%
\label{sub:exercise-1.7.1}
Prove that each of the following sets is measurable and has zero area:
-\subsubsection{\partial{Exercise 1.7.1a}}%
+\subsubsection{\pending{Exercise 1.7.1a}}%
\label{ssub:exercise-1.7.1a}
A set consisting of a single point.
@@ -775,7 +775,7 @@ A set consisting of a single point.
\end{proof}
-\subsubsection{\partial{Exercise 1.7.1b}}%
+\subsubsection{\pending{Exercise 1.7.1b}}%
\label{ssub:exercise-1.7.1b}
A set consisting of a finite number of points in a plane.
@@ -834,7 +834,7 @@ A set consisting of a finite number of points in a plane.
\end{proof}
-\subsubsection{\partial{Exercise 1.7.1c}}%
+\subsubsection{\pending{Exercise 1.7.1c}}%
\label{ssub:exercise-1.7.1c}
The union of a finite collection of line segments in a plane.
@@ -897,7 +897,7 @@ The union of a finite collection of line segments in a plane.
\end{proof}
-\subsection{\partial{Exercise 1.7.2}}%
+\subsection{\pending{Exercise 1.7.2}}%
\label{sub:exercise-1.7.2}
Every right triangular region is measurable because it can be obtained as the
@@ -948,7 +948,7 @@ Prove that every triangular region is measurable and that its area is one half
\end{proof}
-\subsection{\partial{Exercise 1.7.3}}%
+\subsection{\pending{Exercise 1.7.3}}%
\label{sub:exercise-1.7.3}
Prove that every trapezoid and every parallelogram is measurable and derive the
@@ -1053,14 +1053,14 @@ Prove that every trapezoid and every parallelogram is measurable and derive the
\end{proof}
-\subsection{\partial{Exercise 1.7.4}}%
+\subsection{\pending{Exercise 1.7.4}}%
\label{sub:exercise-1.7.4}
Let $P$ be a polygon whose vertices are lattice points.
The area of $P$ is $I + \frac{1}{2}B - 1$, where $I$ denotes the number of
lattice points inside the polygon and $B$ denotes the number on the boundary.
-\subsubsection{\partial{Exercise 1.7.4a}}%
+\subsubsection{\pending{Exercise 1.7.4a}}%
\label{ssub:exercise-1.7.4a}
Prove that the formula is valid for rectangles with sides parallel to the
@@ -1088,7 +1088,7 @@ Prove that the formula is valid for rectangles with sides parallel to the
\end{proof}
-\subsubsection{\partial{Exercise 1.7.4b}}%
+\subsubsection{\pending{Exercise 1.7.4b}}%
\label{ssub:exercise-1.7.4b}
Prove that the formula is valid for right triangles and parallelograms.
@@ -1137,7 +1137,7 @@ Prove that the formula is valid for right triangles and parallelograms.
\end{proof}
-\subsubsection{\partial{Exercise 1.7.4c}}%
+\subsubsection{\pending{Exercise 1.7.4c}}%
\label{ssub:exercise-1.7.4c}
Use induction on the number of edges to construct a proof for general polygons.
@@ -1203,7 +1203,7 @@ Use induction on the number of edges to construct a proof for general polygons.
\end{proof}
-\subsection{\partial{Exercise 1.7.5}}%
+\subsection{\pending{Exercise 1.7.5}}%
\label{sub:exercise-1.7.5}
Prove that a triangle whose vertices are lattice points cannot be equilateral.
@@ -1239,7 +1239,7 @@ ways, using Exercises 2 and 4.]
\end{proof}
-\subsection{\partial{Exercise 1.7.6}}%
+\subsection{\pending{Exercise 1.7.6}}%
\label{sub:exercise-1.7.6}
Let $A = \{1, 2, 3, 4, 5\}$, and let $\mathscr{M}$ denote the class of all
@@ -1324,7 +1324,7 @@ Prove that the set function $n$ satisfies the first three axioms for area.
\section{Exercises 1.11}%
\label{sec:exercises-1-11}
-\subsection{\partial{Exercise 1.11.4}}%
+\subsection{\pending{Exercise 1.11.4}}%
\label{sub:exercise-1.11.4}
Prove that the greatest-integer function has the properties indicated:
@@ -1442,7 +1442,7 @@ $\floor{x + y} = \floor{x} + \floor{y}$ or $\floor{x} + \floor{y} + 1$.
\end{proof}
-\subsubsection{\partial{Exercise 1.11.4d}}%
+\subsubsection{\pending{Exercise 1.11.4d}}%
\label{ssub:exercise-1.11.4d}
$\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$
@@ -1456,7 +1456,7 @@ $\floor{2x} = \floor{x} + \floor{x + \frac{1}{2}}.$
\end{proof}
-\subsubsection{\partial{Exercise 1.11.4e}}%
+\subsubsection{\pending{Exercise 1.11.4e}}%
\label{ssub:exercise-1.11.4e}
$\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$
@@ -1470,7 +1470,7 @@ $\floor{3x} = \floor{x} + \floor{x + \frac{1}{3}} + \floor{x + \frac{2}{3}}.$
\end{proof}
-\subsection{\partial{Hermite's Identity}}%
+\subsection{\pending{Hermite's Identity}}%
\label{sub:hermites-identity}
\label{sub:exercise-1.11.5}
@@ -1559,7 +1559,7 @@ State and prove such a generalization.
\end{proof}
-\subsection{\partial{Exercise 1.11.6}}%
+\subsection{\pending{Exercise 1.11.6}}%
\label{sub:exercise-1.11.6}
Recall that a lattice point $(x, y)$ in the plane is one whose coordinates are
@@ -1602,7 +1602,7 @@ Prove that the number of lattice points in $S$ is equal to the sum
\end{proof}
-\subsection{\partial{Exercise 1.11.7}}%
+\subsection{\pending{Exercise 1.11.7}}%
\label{sub:exercise-1.11.7}
If $a$ and $b$ are positive integers with no common factor, we have the formula
@@ -1612,7 +1612,7 @@ When $b = 1$, the sum on the left is understood to be $0$.
\note{When $b = 1$, the proofs of (a) and (b) are trivial. We continue under the
assumption $b > 1$.}
-\subsubsection{\partial{Exercise 1.11.7a}}%
+\subsubsection{\pending{Exercise 1.11.7a}}%
\label{ssub:exercise-1.11.7a}
Derive this result by a geometric argument, counting lattice points in a right
@@ -1694,7 +1694,7 @@ Derive this result by a geometric argument, counting lattice points in a right
\end{proof}
-\subsubsection{\partial{Exercise 1.11.7b}}%
+\subsubsection{\pending{Exercise 1.11.7b}}%
\label{ssub:exercise-1.11.7b}
Derive the result analytically as follows:
@@ -1736,7 +1736,7 @@ Now apply Exercises 4(a) and (b) to the bracket on the right.
\end{proof}
-\subsection{\partial{Exercise 1.11.8}}%
+\subsection{\pending{Exercise 1.11.8}}%
\label{sub:exercise-1.11.8}
Let $S$ be a set of points on the real line.
@@ -1774,7 +1774,7 @@ This property is described by saying that every step function is a linear
\section{Properties of the Integral of a Step Function}%
\label{sec:properties-integral-step-function}
-\subsection{\partial{Additive Property}}%
+\subsection{\pending{Additive Property}}%
\label{sub:step-additive-property}
\label{sub:theorem-1.2}
@@ -1817,7 +1817,7 @@ This property is described by saying that every step function is a linear
\end{proof}
-\subsection{\partial{Homogeneous Property}}%
+\subsection{\pending{Homogeneous Property}}%
\label{sub:step-homogeneous-property}
\label{sub:theorem-1.3}
@@ -1848,7 +1848,7 @@ This property is described by saying that every step function is a linear
\end{proof}
-\subsection{\partial{Linearity Property}}%
+\subsection{\pending{Linearity Property}}%
\label{sub:step-linearity-property}
\label{sub:theorem-1.4}
@@ -1878,7 +1878,7 @@ This property is described by saying that every step function is a linear
\end{proof}
-\subsection{\partial{Comparison Theorem}}%
+\subsection{\pending{Comparison Theorem}}%
\label{sub:step-comparison-theorem}
\label{sub:theorem-1.5}
@@ -1917,7 +1917,7 @@ This property is described by saying that every step function is a linear
\end{proof}
-\subsection{\partial{Additivity With Respect to the Interval of Integration}}%
+\subsection{\pending{Additivity With Respect to the Interval of Integration}}%
\label{sub:step-additivity-with-respect-interval-integration}
\label{sub:theorem-1.6}
@@ -1963,7 +1963,7 @@ This property is described by saying that every step function is a linear
\end{proof}
-\subsection{\partial{Invariance Under Translation}}%
+\subsection{\pending{Invariance Under Translation}}%
\label{sub:step-invariance-under-translation}
\label{sub:theorem-1.7}
@@ -2004,7 +2004,7 @@ This property is described by saying that every step function is a linear
\end{proof}
-\subsection{\partial{Expansion or Contraction of the Interval of Integration}}%
+\subsection{\pending{Expansion or Contraction of the Interval of Integration}}%
\label{sub:step-expansion-contraction-interval-integration}
\label{sub:theorem-1.8}
@@ -2064,7 +2064,7 @@ This property is described by saying that every step function is a linear
\end{proof}
-\subsection{\partial{Reflection Property}}%
+\subsection{\pending{Reflection Property}}%
\label{sub:step-reflection-property}
Let $s$ be a step function on closed interval $[a, b]$.
@@ -2085,12 +2085,12 @@ Then
\section{Exercises 1.15}%
\label{sec:exercises-1.15}
-\subsection{\partial{Exercise 1.15.1}}%
+\subsection{\pending{Exercise 1.15.1}}%
\label{sub:exercise-1.15.1}
Compute the value of each of the following integrals.
-\subsubsection{\partial{Exercise 1.15.1a}}%
+\subsubsection{\pending{Exercise 1.15.1a}}%
\label{ssub:exercise-1.15.1a}
$\int_{-1}^3 \floor{x} \mathop{dx}$.
@@ -2112,7 +2112,7 @@ $\int_{-1}^3 \floor{x} \mathop{dx}$.
\end{proof}
-\subsubsection{\partial{Exercise 1.15.1c}}%
+\subsubsection{\pending{Exercise 1.15.1c}}%
\label{ssub:exercise-1.15.1c}
$\int_{-1}^3 \left(\floor{x} + \floor{x + \frac{1}{2}}\right) \mathop{dx}$.
@@ -2140,7 +2140,7 @@ $\int_{-1}^3 \left(\floor{x} + \floor{x + \frac{1}{2}}\right) \mathop{dx}$.
\end{proof}
-\subsubsection{\partial{Exericse 1.15.1e}}%
+\subsubsection{\pending{Exericse 1.15.1e}}%
\label{ssub:exercise-1.15.1e}
$\int_{-1}^3 \floor{2x} \mathop{dx}$.
@@ -2155,7 +2155,7 @@ $\int_{-1}^3 \floor{2x} \mathop{dx}$.
\end{proof}
-\subsection{\partial{Exercise 1.15.3}}%
+\subsection{\pending{Exercise 1.15.3}}%
\label{sub:exercise-1.15.3}
Show that
@@ -2186,10 +2186,10 @@ Show that
\end{proof}
-\subsection{\partial{Exercise 1.15.5}}%
+\subsection{\pending{Exercise 1.15.5}}%
\label{sub:exercise-1.15.5}
-\subsubsection{\partial{Exercise 1.15.5a}}%
+\subsubsection{\pending{Exercise 1.15.5a}}%
\label{ssub:exercise-1.15.5a}
Prove that $\int_0^2 \floor{t^2} \mathop{dt} = 5 - \sqrt{2} - \sqrt{3}$.
@@ -2212,7 +2212,7 @@ Prove that $\int_0^2 \floor{t^2} \mathop{dt} = 5 - \sqrt{2} - \sqrt{3}$.
\end{proof}
-\subsubsection{\partial{Exercise 1.15.5b}}%
+\subsubsection{\pending{Exercise 1.15.5b}}%
\label{ssub:exercise-1.15.5b}
Compute $\int_{-3}^3 \floor{t^2} \mathop{dt}$.
@@ -2256,10 +2256,10 @@ Compute $\int_{-3}^3 \floor{t^2} \mathop{dt}$.
\end{proof}
-\subsection{\partial{Exercise 1.15.7}}%
+\subsection{\pending{Exercise 1.15.7}}%
\label{sub:exercise-1.15.7}
-\subsubsection{\partial{Exercise 1.15.7a}}%
+\subsubsection{\pending{Exercise 1.15.7a}}%
\label{ssub:exercise-1.15.7a}
Compute $\int_0^9 \floor{\sqrt{t}} \mathop{dt}$.
@@ -2281,7 +2281,7 @@ Compute $\int_0^9 \floor{\sqrt{t}} \mathop{dt}$.
\end{proof}
-\subsubsection{\partial{Exercise 1.15.7b}}%
+\subsubsection{\pending{Exercise 1.15.7b}}%
\label{ssub:exercise-1.15.7b}
If $n$ is a positive integer, prove that
@@ -2356,7 +2356,7 @@ If $n$ is a positive integer, prove that
\end{proof}
-\subsection{\partial{Exercise 1.15.9}}%
+\subsection{\pending{Exercise 1.15.9}}%
\label{sub:exercise-1.15.9}
Show that the following property is equivalent to
@@ -2378,7 +2378,7 @@ Show that the following property is equivalent to
\end{proof}
-\subsection{\partial{Exercise 1.15.11}}%
+\subsection{\pending{Exercise 1.15.11}}%
\label{sub:exercise-1.15.11}
If we instead defined the integral of step functions as
@@ -2389,7 +2389,7 @@ If we instead defined the integral of step functions as
a new and different theory of integration would result.
Which of the following properties would remain valid in this new theory?
-\subsubsection{\partial{Exercise 1.15.11a}}%
+\subsubsection{\pending{Exercise 1.15.11a}}%
\label{ssub:exercise-1.15.11a}
$\int_a^b s + \int_b^c s = \int_a^c s$.
@@ -2425,7 +2425,7 @@ $\int_a^b s + \int_b^c s = \int_a^c s$.
\end{proof}
-\subsubsection{\partial{Exercise 1.15.11b}}%
+\subsubsection{\pending{Exercise 1.15.11b}}%
\label{ssub:exercise-1.15.11b}
$\int_a^b (s + t) = \int_a^b s + \int_a^b t$.
@@ -2472,7 +2472,7 @@ $\int_a^b (s + t) = \int_a^b s + \int_a^b t$.
\end{proof}
-\subsubsection{\partial{Exercise 1.15.11c}}%
+\subsubsection{\pending{Exercise 1.15.11c}}%
\label{ssub:exercise-1.15.11c}
$\int_a^b c \cdot s = c \int_a^b s$.
@@ -2504,7 +2504,7 @@ $\int_a^b c \cdot s = c \int_a^b s$.
\end{proof}
-\subsubsection{\partial{Exercise 1.15.11d}}%
+\subsubsection{\pending{Exercise 1.15.11d}}%
\label{ssub:exercise-1.15.11d}
$\int_{a+c}^{b+c} s(x) \mathop{dx} = \int_a^b s(x + c) \mathop{dx}$.
@@ -2542,7 +2542,7 @@ $\int_{a+c}^{b+c} s(x) \mathop{dx} = \int_a^b s(x + c) \mathop{dx}$.
\end{proof}
-\subsubsection{\partial{Exercise 1.15.11e}}%
+\subsubsection{\pending{Exercise 1.15.11e}}%
\label{ssub:exercise-1.15.11e}
If $s(x) < t(x)$ for each $x$ in $[a, b]$, then $\int_a^b s < \int_a^b t$.
@@ -2583,7 +2583,7 @@ If $s(x) < t(x)$ for each $x$ in $[a, b]$, then $\int_a^b s < \int_a^b t$.
\section{Upper and Lower Integrals}%
\label{sec:upper-lower-integrals}
-\subsection{\partial{Theorem 1.9}}%
+\subsection{\pending{Theorem 1.9}}%
\label{sub:theorem-1.9}
\begin{theorem}[1.9]
@@ -2649,7 +2649,7 @@ If $s(x) < t(x)$ for each $x$ in $[a, b]$, then $\int_a^b s < \int_a^b t$.
\section{The Area of an Ordinate Set Expressed as an Integral}%
\label{sec:area-ordinate-set-expressed-integral}
-\subsection{\partial{Theorem 1.10}}%
+\subsection{\pending{Theorem 1.10}}%
\label{sub:theorem-1.10}
\begin{theorem}[1.10]
@@ -2676,7 +2676,7 @@ If $s(x) < t(x)$ for each $x$ in $[a, b]$, then $\int_a^b s < \int_a^b t$.
\end{proof}
-\subsection{\partial{Theorem 1.11}}%
+\subsection{\pending{Theorem 1.11}}%
\label{sub:theorem-1.11}
\begin{theorem}[1.11]
@@ -2733,7 +2733,7 @@ If $s(x) < t(x)$ for each $x$ in $[a, b]$, then $\int_a^b s < \int_a^b t$.
{Integrability of Bounded Monotonic \texorpdfstring{\\}{}Functions}
\label{sec:integrability-bounded-monotonic-functions}
-\subsection{\partial{Theorem 1.12}}%
+\subsection{\pending{Theorem 1.12}}%
\label{sub:theorem-1.12}
\begin{theorem}[1.12]
@@ -2837,7 +2837,7 @@ If $s(x) < t(x)$ for each $x$ in $[a, b]$, then $\int_a^b s < \int_a^b t$.
\end{proof}
-\subsection{\partial{Theorem 1.13}}%
+\subsection{\pending{Theorem 1.13}}%
\label{sub:theorem-1.13}
\begin{theorem}[1.13]
@@ -2909,7 +2909,7 @@ If $s(x) < t(x)$ for each $x$ in $[a, b]$, then $\int_a^b s < \int_a^b t$.
\end{proof}
-\subsection{\partial{Theorem 1.14}}%
+\subsection{\pending{Theorem 1.14}}%
\label{sub:theorem-1.14}
\begin{theorem}[1.14]
@@ -2981,7 +2981,7 @@ If $s(x) < t(x)$ for each $x$ in $[a, b]$, then $\int_a^b s < \int_a^b t$.
\end{proof}
-\subsection{\unverified{%
+\subsection{\sorry{%
Integral of \texorpdfstring{$\int_0^b x^p \mathop{dx}$}{int-x-p} when
\texorpdfstring{$p$}{p} is a Positive Integer}}%
\label{sub:calculation-integral-int-x-p-p-positive-integer}
diff --git a/Bookshelf/Enderton/Logic.tex b/Bookshelf/Enderton/Logic.tex
index d2ba7d2..b79caf4 100644
--- a/Bookshelf/Enderton/Logic.tex
+++ b/Bookshelf/Enderton/Logic.tex
@@ -23,7 +23,7 @@
\chapter{Useful Facts About Sets}%
\label{chap:useful-facts-about-sets}
-\section{\unverified{Lemma 0A}}%
+\section{\sorry{Lemma 0A}}%
\label{sec:lemma-0a}
Assume that $\langle x_1, \ldots, x_m \rangle =
diff --git a/Bookshelf/Enderton/Set.tex b/Bookshelf/Enderton/Set.tex
index 5caf9ce..7fb94ce 100644
--- a/Bookshelf/Enderton/Set.tex
+++ b/Bookshelf/Enderton/Set.tex
@@ -25,13 +25,13 @@
\chapter{Reference}%
\label{chap:reference}
-\section{\partial{Axiom of Choice, First Form}}%
+\section{\pending{Axiom of Choice, First Form}}%
\label{ref:axiom-of-choice-1}
For any relation $R$ there is a function $H \subseteq R$ with
$\dom{H} = \dom{R}$.
-\section{\partial{Axiom of Choice, Second Form}}%
+\section{\pending{Axiom of Choice, Second Form}}%
\label{ref:axiom-of-choice-2}
For any set $I$ and any function $H$ with domain $I$, if $H(i) \neq \emptyset$
@@ -73,7 +73,7 @@ There is a set having no members:
\end{axiom}
-\section{\partial{Equivalence Relation}}%
+\section{\pending{Equivalence Relation}}%
\label{ref:equivalence-relation}
Relation $R$ is an \textbf{equivalence relation} if and only if $R$ is a binary
@@ -242,7 +242,7 @@ Given \nameref{ref:relation} $R$, the \textbf{range} of $R$, denoted $\ran{R}$,
\end{definition}
-\section{\partial{Reflexive Relation}}%
+\section{\pending{Reflexive Relation}}%
\label{ref:reflexive-relation}
A binary relation $R$ is \textbf{reflexive} on $A$ if and only if $xRx$ for all
@@ -284,7 +284,7 @@ For each formula $\phi$ not containing $B$, the following is an axiom:
\end{axiom}
-\section{\partial{Symmetric Relation}}%
+\section{\pending{Symmetric Relation}}%
\label{ref:symmetric-relation}
A binary relation $R$ is \textbf{symmetric} on $A$ if and only if whenever
@@ -302,7 +302,7 @@ The \textbf{symmetric difference} $A + B$ of sets $A$ and $B$ is the set
\end{definition}
-\section{\partial{Transitive Relation}}%
+\section{\pending{Transitive Relation}}%
\label{ref:transitive-relation}
A binary relation $R$ is \textbf{transitive} on $A$ if and only if whenever
@@ -505,7 +505,7 @@ Show that $\{\{x\}, \{x, y\}\} \in \powerset{\powerset{B}}.$
\end{proof}
-\subsection{\partial{Exercise 1.5}}%
+\subsection{\unverified{Exercise 1.5}}%
\label{sub:exercise-1.5}
Define the rank of a set $c$ to be the least $\alpha$ such that
@@ -545,7 +545,7 @@ Compute the rank of
\end{proof}
-\subsection{\partial{Exercise 1.6}}%
+\subsection{\unverified{Exercise 1.6}}%
\label{sub:exercise-1.6}
We have stated that $V_{\alpha + 1} = A \cup \powerset{V_\alpha}$.
@@ -593,7 +593,7 @@ Prove this at least for $\alpha < 3$.
\end{proof}
-\subsection{\partial{Exercise 1.7}}%
+\subsection{\unverified{Exercise 1.7}}%
\label{sub:exercise-1.7}
List all the members of $V_3$.
@@ -641,7 +641,7 @@ List all the members of $V_4$.
\section{Axioms}%
\label{sec:axioms}
-\subsection{\partial{Theorem 2A}}%
+\subsection{\unverified{Theorem 2A}}%
\label{sub:theorem-2a}
\begin{theorem}[2A]
@@ -665,7 +665,7 @@ List all the members of $V_4$.
\end{proof}
-\subsection{\partial{Theorem 2B}}%
+\subsection{\unverified{Theorem 2B}}%
\label{sub:theorem-2b}
\begin{theorem}[2B]
@@ -1103,7 +1103,7 @@ For any sets $A$, $B$, and $C$,
\end{proof}
-\subsection{\partial{General Distributive Laws}}%
+\subsection{\unverified{General Distributive Laws}}%
\label{sub:general-distributive-laws}
For any sets $A$ and $\mathscr{B}$,
@@ -1163,7 +1163,7 @@ For any sets $A$ and $\mathscr{B}$,
\end{proof}
-\subsection{\partial{General De Morgan's Laws}}%
+\subsection{\unverified{General De Morgan's Laws}}%
\label{sub:general-de-morgans-laws}
For any set $C$ and $\mathscr{A} \neq \emptyset$,
@@ -1590,7 +1590,7 @@ Under what conditions does equality hold?
\end{proof}
-\subsection{\partial{Exercise 2.8}}%
+\subsection{\unverified{Exercise 2.8}}%
\label{sub:exercise-2.8}
Show that there is no set to which every singleton (that is, every set of the
@@ -1990,7 +1990,7 @@ Show that the following four conditions are equivalent.
\end{proof}
-\subsection{\partial{Exercise 2.18}}%
+\subsection{\unverified{Exercise 2.18}}%
\label{sub:exercise-2.18}
Assume that $A$ and $B$ are subsets of $S$.
@@ -2195,7 +2195,7 @@ Show that if $A$ and $B$ are nonempty sets, then
\end{proof}
-\subsection{\partial{Exercise 2.23}}%
+\subsection{\unverified{Exercise 2.23}}%
\label{sub:exercise-2.23}
Show that if $\mathscr{B}$ is nonempty, then
@@ -2856,7 +2856,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
\end{proof}
-\subsection{\partial{Theorem 3J}}%
+\subsection{\pending{Theorem 3J}}%
\label{sub:theorem-3j}
\begin{theorem}[3J]
@@ -2942,7 +2942,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
\end{proof}
-\subsection{\partial{Theorem 3K(a)}}%
+\subsection{\pending{Theorem 3K(a)}}%
\label{sub:theorem-3k-a}
\begin{theorem}[3K(a)]
@@ -3010,7 +3010,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
\end{proof}
-\subsection{\partial{Theorem 3K(b)}}%
+\subsection{\pending{Theorem 3K(b)}}%
\label{sub:theorem-3k-b}
\begin{theorem}[3K(b)]
@@ -3093,7 +3093,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
\end{proof}
-\subsection{\partial{Theorem 3K(c)}}%
+\subsection{\pending{Theorem 3K(c)}}%
\label{sub:theorem-3k-c}
\begin{theorem}[3K(c)]
@@ -3143,7 +3143,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
\end{proof}
-\subsection{\partial{Corollary 3L}}%
+\subsection{\pending{Corollary 3L}}%
\label{sub:corollary-3l}
\begin{theorem}[3L]
@@ -3175,7 +3175,7 @@ For any one-to-one function $F$, $F^{-1}$ is also one-to-one.
\section{Equivalence Relations}%
\label{sec:equivalence-relations}
-\subsection{\unverified{Theorem 3M}}%
+\subsection{\sorry{Theorem 3M}}%
\label{sub:theorem-3m}
\begin{theorem}[3M]
@@ -3327,7 +3327,7 @@ Show that $A \times \bigcup \mathscr{B} =
\end{proof}
-\subsection{\partial{Exercise 3.4}}%
+\subsection{\unverified{Exercise 3.4}}%
\label{sub:exercise-3.4}
Show that there is no set to which every ordered pair belongs.
@@ -3656,7 +3656,7 @@ Discuss the result of replacing the union operation by the intersection
\end{answer}
-\subsection{\partial{Exercise 3.10}}%
+\subsection{\unverified{Exercise 3.10}}%
\label{sub:exercise-3.10}
Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
@@ -3681,7 +3681,7 @@ Show that an ordered $4$-tuple is also an ordered $m$-tuple for every positive
\end{answer}
-\subsection{\unverified{Exercise 3.11}}%
+\subsection{\sorry{Exercise 3.11}}%
\label{sub:exercise-3.11}
Prove the following version (for functions) of the extensionality principle:
@@ -3695,7 +3695,7 @@ Then $F = G$.
\end{proof}
-\subsection{\unverified{Exercise 3.12}}%
+\subsection{\sorry{Exercise 3.12}}%
\label{sub:exercise-3.12}
Assume that $f$ and $g$ are functions and show that
@@ -3708,7 +3708,7 @@ Assume that $f$ and $g$ are functions and show that
\end{proof}
-\subsection{\unverified{Exercise 3.13}}%
+\subsection{\sorry{Exercise 3.13}}%
\label{sub:exercise-3.13}
Assume that $f$ and $g$ are functions with $f \subseteq g$ and
@@ -3721,7 +3721,7 @@ Show that $f = g$.
\end{proof}
-\subsection{\unverified{Exercise 3.14}}%
+\subsection{\sorry{Exercise 3.14}}%
\label{sub:exercise-3.14}
Assume that $f$ and $g$ are functions.
@@ -3738,7 +3738,7 @@ Assume that $f$ and $g$ are functions.
\end{proof}
-\subsection{\unverified{Exercise 3.15}}%
+\subsection{\sorry{Exercise 3.15}}%
\label{sub:exercise-3.15}
Let $\mathscr{A}$ be a set of functions such that for any $f$ and $g$ in
@@ -3751,7 +3751,7 @@ Show that $\bigcup \mathscr{A}$ is a function.
\end{proof}
-\subsection{\unverified{Exercise 3.16}}%
+\subsection{\sorry{Exercise 3.16}}%
\label{sub:exercise-3.16}
Show that there is no set to which every function belongs.
@@ -3762,7 +3762,7 @@ Show that there is no set to which every function belongs.
\end{proof}
-\subsection{\unverified{Exercise 3.17}}%
+\subsection{\sorry{Exercise 3.17}}%
\label{sub:exercise-3.17}
Show that the composition of two single-rooted sets is again single-rooted.
@@ -3774,7 +3774,7 @@ Conclude that the composition of two one-to-one functions is again one-to-one.
\end{proof}
-\subsection{\unverified{Exercise 3.18}}%
+\subsection{\sorry{Exercise 3.18}}%
\label{sub:exercise-3.18}
Let $R$ be the set
@@ -3789,7 +3789,7 @@ Evaluate the following: $R \circ R$, $R \restriction \{1\}$,
\end{proof}
-\subsection{\unverified{Exercise 3.19}}%
+\subsection{\sorry{Exercise 3.19}}%
\label{sub:exercise-3.19}
Let $$A = \{
@@ -3808,7 +3808,7 @@ Evaluate each of the following: $A(\emptyset)$, $\img{A}{\emptyset}$,
\end{proof}
-\subsection{\unverified{Exercise 3.20}}%
+\subsection{\sorry{Exercise 3.20}}%
\label{sub:exercise-3.20}
Show that $F \restriction A = F \cap (A \times \ran{F})$.
@@ -3819,7 +3819,7 @@ Show that $F \restriction A = F \cap (A \times \ran{F})$.
\end{proof}
-\subsection{\unverified{Exercise 3.21}}%
+\subsection{\sorry{Exercise 3.21}}%
\label{sub:exercise-3.21}
Show that $(R \circ S) \circ T = R \circ (S \circ T)$.
@@ -3830,7 +3830,7 @@ Show that $(R \circ S) \circ T = R \circ (S \circ T)$.
\end{proof}
-\subsection{\unverified{Exercise 3.22}}%
+\subsection{\sorry{Exercise 3.22}}%
\label{sub:exercise-3.22}
Show that the following are correct for any sets.
@@ -3848,7 +3848,7 @@ Show that the following are correct for any sets.
\end{proof}
-\subsection{\unverified{Exercise 3.23}}%
+\subsection{\sorry{Exercise 3.23}}%
\label{sub:exercise-3.23}
Let $I_A$ be the identity function on the set $A$.
@@ -3862,7 +3862,7 @@ Show that for any sets $B$ and $C$,
\end{proof}
-\subsection{\unverified{Exercise 3.24}}%
+\subsection{\sorry{Exercise 3.24}}%
\label{sub:exercise-3.24}
Show that for a function $F$,
@@ -3874,7 +3874,7 @@ Show that for a function $F$,
\end{proof}
-\subsection{\unverified{Exercise 3.25}}%
+\subsection{\sorry{Exercise 3.25}}%
\label{sub:exercise-3.25}
\begin{enumerate}[(a)]
@@ -3891,7 +3891,7 @@ Show that for a function $F$,
\end{proof}
-\subsection{\unverified{Exercise 3.26}}%
+\subsection{\sorry{Exercise 3.26}}%
\label{sub:exercise-3.26}
Prove the second halves of parts (a) and (b) of Theorem 3K.
@@ -3902,7 +3902,7 @@ Prove the second halves of parts (a) and (b) of Theorem 3K.
\end{proof}
-\subsection{\unverified{Exercise 3.27}}%
+\subsection{\sorry{Exercise 3.27}}%
\label{sub:exercise-3.27}
Show that $\dom{(F \circ G)} = \img{G^{-1}}{\dom{F}}$ for any sets $F$ and $G$.
@@ -3914,7 +3914,7 @@ Show that $\dom{(F \circ G)} = \img{G^{-1}}{\dom{F}}$ for any sets $F$ and $G$.
\end{proof}
-\subsection{\unverified{Exercise 3.28}}%
+\subsection{\sorry{Exercise 3.28}}%
\label{sub:exercise-3.28}
Assume that $f$ is a one-to-one function from $A$ into $B$, and that $G$ is the
@@ -3928,7 +3928,7 @@ Show that $G$ maps $\powerset{A}$ one-to-one into $\powerset{B}$.
\end{proof}
-\subsection{\unverified{Exercise 3.29}}%
+\subsection{\sorry{Exercise 3.29}}%
\label{sub:exercise-3.29}
Assume that $f \colon A \rightarrow B$ and define a function
@@ -3943,7 +3943,7 @@ Does the converse hold?
\end{proof}
-\subsection{\unverified{Exercise 3.30}}%
+\subsection{\sorry{Exercise 3.30}}%
\label{sub:exercise-3.30}
Assume that $F \colon \powerset{A} \rightarrow \powerset{A}$ and that $F$ has
@@ -3963,7 +3963,7 @@ Define
\end{proof}
-\subsection{\unverified{Exercise 3.31}}%
+\subsection{\sorry{Exercise 3.31}}%
\label{sub:exercise-3.31}
Show that from the first form of the axiom of choice we can prove the second
diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
index 28fdc0f..1bffd23 100644
--- a/DocGen4/Output/Index.lean
+++ b/DocGen4/Output/Index.lean
@@ -47,11 +47,15 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
statements, theorems, lemmas, etc. that have been proven in both
LaTeX and Lean.
+
+ Olive statements are reserved for
+ statements, theorems, lemmas, etc. that have been proven in LaTeX
+ and will not be proven in Lean.
+
Fuchsia statements are reserved
for definitions, axioms, statements, theorems, lemmas, etc. that
- have been proven or encoded in LaTeX but not yet proven or encoded
- in Lean.
+ have been proven or encoded in LaTeX and will be encoded in Lean.
Maroon serves as a catch-all for
diff --git a/preamble.tex b/preamble.tex
index 4a6203e..fc384eb 100644
--- a/preamble.tex
+++ b/preamble.tex
@@ -118,9 +118,11 @@
\texorpdfstring{\color{darkgray}\faParagraph\ #1}{#1}}
\DeclareRobustCommand{\verified}[1]{%
\texorpdfstring{\color{teal}\faCheckCircle\ #1}{#1}}
-\DeclareRobustCommand{\partial}[1]{%
- \texorpdfstring{\color{Fuchsia}\faPencil*\ #1}{#1}}
\DeclareRobustCommand{\unverified}[1]{%
+ \texorpdfstring{\color{olive}\faCheckCircle[regular]\ #1}{#1}}
+\DeclareRobustCommand{\pending}[1]{%
+ \texorpdfstring{\color{Fuchsia}\faPencil*\ #1}{#1}}
+\DeclareRobustCommand{\sorry}[1]{%
\texorpdfstring{\color{Maroon}\faExclamationCircle\ #1}{#1}}
% ========================================