summaryrefslogtreecommitdiff
path: root/library/ordinal.tex
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2025-07-08 22:16:01 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2025-07-08 22:16:01 +0200
commitda6d425281534407a92ce18a22584905a7847a39 (patch)
tree2449971b42b96b566039e0c2c9a575481ae51f38 /library/ordinal.tex
parent9d34eebafc87e6bce476ccc487a88b440315089b (diff)
Update lemma name
Diffstat (limited to 'library/ordinal.tex')
-rw-r--r--library/ordinal.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/ordinal.tex b/library/ordinal.tex
index 6f924c1..c092fa8 100644
--- a/library/ordinal.tex
+++ b/library/ordinal.tex
@@ -559,7 +559,7 @@ Then $\alpha\subseteq\beta$.
\end{lemma}
\begin{proof}
Suppose not.
- Then $\emptyset\precedes \emptyset$ by \cref{notin_emptyset,limit_ordinal}.
+ Then $\emptyset\precedes \emptyset$ by \cref{emptyset,limit_ordinal}.
Thus $\emptyset\in \emptyset$.
Contradiction.
\end{proof}
@@ -636,4 +636,4 @@ Then $\alpha\subseteq\beta$.
% $\emptyset\precedes \naturals$.
% If $n\in \naturals$, then $\suc{n}\in\naturals$.
%\end{proof}
-% \ No newline at end of file
+%