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

---
 library/nat.tex | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 library/nat.tex

(limited to 'library/nat.tex')

diff --git a/library/nat.tex b/library/nat.tex
new file mode 100644
index 0000000..529ba54
--- /dev/null
+++ b/library/nat.tex
@@ -0,0 +1,21 @@
+\import{set/suc.tex}
+
+
+\section{Natural numbers}
+
+\begin{abbreviation}\label{inductive_set}
+    $A$ is an inductive set iff $\emptyset\in A$ and for all $a\in A$ we have $\suc{a}\in A$.
+\end{abbreviation}
+
+\begin{axiom}\label{naturals_inductive_set}
+    $\naturals$ is an inductive set.
+\end{axiom}
+
+\begin{axiom}\label{naturals_smallest_inductive_set}
+    Let $A$ be an inductive set.
+    Then $\naturals\subseteq A$.
+\end{axiom}
+
+\begin{abbreviation}\label{naturalnumber}
+    $n$ is a natural number iff $n\in\naturals$.
+\end{abbreviation}
-- 
cgit v1.2.3