diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-05 14:58:32 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-08-05 14:58:32 +0200 |
| commit | db5e4920b8b1f0fbc08bf78708ee3076ea895b75 (patch) | |
| tree | ded256ed890959f7f4a63d0b5f61be145b7b3842 /test/phase5/exact-cases-contradiction.tex | |
| parent | ac5e2b469436f2f1f9a15b3db316dbef431ff3c2 (diff) | |
Restore exact cases and contradiction
Diffstat (limited to 'test/phase5/exact-cases-contradiction.tex')
| -rw-r--r-- | test/phase5/exact-cases-contradiction.tex | 45 |
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} |
