diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/set/cantor.tex | 2 | ||||
| -rw-r--r-- | library/set/regularity.tex | 2 |
2 files changed, 1 insertions, 3 deletions
diff --git a/library/set/cantor.tex b/library/set/cantor.tex index 5455e70..093adee 100644 --- a/library/set/cantor.tex +++ b/library/set/cantor.tex @@ -16,7 +16,5 @@ Take $a'$ such that $a'\in A$ and $f(a') = B$ by \cref{surj}. We have if $a'\in B$, then $a'\notin B$ by assumption. We have if $a'\notin B$, then $a'\in B$ by assumption. - We have $a'\in B$ by assumption. - We have $a'\notin B$ by assumption. Contradiction by assumption. \end{proof} diff --git a/library/set/regularity.tex b/library/set/regularity.tex index 440467d..907bf57 100644 --- a/library/set/regularity.tex +++ b/library/set/regularity.tex @@ -28,7 +28,7 @@ \end{proof} -% Isabelle/ZF-style foundation for case analysis +% Foundation for case analysis \begin{theorem}[Foundation]\label{foundation} Let $A$ be a set. Then $A = \emptyset$ or there exists $a\in A$ |