summaryrefslogtreecommitdiff
path: root/test/examples/formula.tex
diff options
context:
space:
mode:
authoradelon <22380201+adelon@users.noreply.github.com>2024-05-07 18:07:23 +0200
committeradelon <22380201+adelon@users.noreply.github.com>2024-05-07 18:07:23 +0200
commitb2f9f7900ccb4a569ed23e9ecf327564dbba2b7d (patch)
treeac781463be5cf38ed785cd22339a291ccf7cdec8 /test/examples/formula.tex
parentbc2ea0a384548aab50991c4de365f1afbad9a284 (diff)
Sketch noun coord, symbols for reals
Diffstat (limited to 'test/examples/formula.tex')
-rw-r--r--test/examples/formula.tex4
1 files changed, 4 insertions, 0 deletions
diff --git a/test/examples/formula.tex b/test/examples/formula.tex
index c029402..e3b1e29 100644
--- a/test/examples/formula.tex
+++ b/test/examples/formula.tex
@@ -5,3 +5,7 @@
\begin{proposition}\label{formula_test_exists}
$\exists x, y. x = y$.
\end{proposition}
+
+\begin{proposition}\label{formula_test_not_exists}
+ $\exists x, y. x = y$ if and only if not $\exists x. x \neq x$.
+\end{proposition}