summaryrefslogtreecommitdiff
path: root/test/phase5/exact-cases-contradiction.tex
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2026-08-05 14:58:32 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2026-08-05 14:58:32 +0200
commitdb5e4920b8b1f0fbc08bf78708ee3076ea895b75 (patch)
treeded256ed890959f7f4a63d0b5f61be145b7b3842 /test/phase5/exact-cases-contradiction.tex
parentac5e2b469436f2f1f9a15b3db316dbef431ff3c2 (diff)
Restore exact cases and contradiction
Diffstat (limited to 'test/phase5/exact-cases-contradiction.tex')
-rw-r--r--test/phase5/exact-cases-contradiction.tex45
1 files changed, 45 insertions, 0 deletions
diff --git a/test/phase5/exact-cases-contradiction.tex b/test/phase5/exact-cases-contradiction.tex
new file mode 100644
index 0000000..1752139
--- /dev/null
+++ b/test/phase5/exact-cases-contradiction.tex
@@ -0,0 +1,45 @@
+\begin{proposition}\label{cases_exact}
+ Let $A$ be a set.
+ $A=A$.
+\end{proposition}
+\begin{proof}
+ \begin{byCase}
+ \caseOf{$A=\emptyset$.}
+ Follows.
+ \caseOf{$A=\{A\}$.}
+ Follows.
+ \caseOf{$A=A$.}
+ Follows.
+ \end{byCase}
+\end{proof}
+
+\begin{proposition}\label{by_contradiction_exact}
+ Let $A$ be a set.
+ $A=A$.
+\end{proposition}
+\begin{proof}
+ Suppose not.
+ Contradiction.
+\end{proof}
+
+\begin{proposition}\label{arbitrary_contradiction_exact}
+ Let $A$ be a set.
+ Suppose $A\neq A$.
+ Then $A=A$.
+\end{proposition}
+\begin{proof}
+ Contradiction.
+\end{proof}
+
+\begin{proposition}\label{omitted_case_exact}
+ Let $A$ be a set.
+ $A=A$.
+\end{proposition}
+\begin{proof}
+ \begin{byCase}
+ \caseOf{$A=A$.}
+ Omitted.
+ \caseOf{$A\neq A$.}
+ Follows.
+ \end{byCase}
+\end{proof}