From 442d732696ad431b84f6e5c72b6ee785be4fd968 Mon Sep 17 00:00:00 2001
From: adelon <22380201+adelon@users.noreply.github.com>
Date: Sat, 10 Feb 2024 02:22:14 +0100
Subject: Initial commit

---
 megalodon/scraps.tex | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 megalodon/scraps.tex

(limited to 'megalodon/scraps.tex')

diff --git a/megalodon/scraps.tex b/megalodon/scraps.tex
new file mode 100644
index 0000000..f79a630
--- /dev/null
+++ b/megalodon/scraps.tex
@@ -0,0 +1,17 @@
+\begin{axiom}\label{trivial}
+    For all $x$ we have $x = x$.
+\end{axiom}
+
+% Axiom EmptyAx : ~exists x:set, x :e Empty.
+\begin{axiom}\label{empty_axiom}
+    There exists no set $x$ such that $x\in\emptyset$.
+\end{axiom}
+
+% UnionEq : forall X x, x :e Union X <-> exists Y, x :e Y /\ Y :e X.
+\begin{axiom}\label{union_eq}
+    For all $x, X$ we have $x\in\unions{X}$ iff there exists $Y$ such that $x\in Y\in X$.
+\end{axiom}
+
+\begin{theorem}\label{eq_refl}
+    For all $x$ we have $x=x$.
+\end{theorem}
-- 
cgit v1.2.3