From 29f32e2031eafa087323d79d812a1b38ac78f977 Mon Sep 17 00:00:00 2001 From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com> Date: Mon, 23 Sep 2024 01:20:05 +0200 Subject: working commit --- library/nat.tex | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'library/nat.tex') diff --git a/library/nat.tex b/library/nat.tex index ac9a141..841ac36 100644 --- a/library/nat.tex +++ b/library/nat.tex @@ -3,48 +3,48 @@ \section{Natural numbers} -\begin{abbreviation}\label{inductive_set} +\begin{abbreviation}\label{num_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} +\begin{axiom}\label{num_naturals_inductive_set} $\naturals$ is an inductive set. \end{axiom} -\begin{axiom}\label{naturals_smallest_inductive_set} +\begin{axiom}\label{num_naturals_smallest_inductive_set} Let $A$ be an inductive set. Then $\naturals\subseteq A$. \end{axiom} -\begin{abbreviation}\label{naturalnumber} +\begin{abbreviation}\label{num_naturalnumber} $n$ is a natural number iff $n\in \naturals$. \end{abbreviation} -\begin{lemma}\label{emptyset_in_naturals} +\begin{lemma}\label{num_emptyset_in_naturals} $\emptyset\in\naturals$. \end{lemma} -\begin{signature}\label{addition_is_set} +\begin{signature}\label{num_addition_is_set} $x+y$ is a set. \end{signature} -\begin{axiom}\label{addition_on_naturals} +\begin{axiom}\label{num_addition_on_naturals} $x+y$ is a natural number iff $x$ is a natural number and $y$ is a natural number. \end{axiom} -\begin{abbreviation}\label{zero_is_emptyset} +\begin{abbreviation}\label{num_zero_is_emptyset} $\zero = \emptyset$. \end{abbreviation} -\begin{axiom}\label{addition_axiom_1} +\begin{axiom}\label{num_addition_axiom_1} For all $x \in \naturals$ $x + \zero = \zero + x = x$. \end{axiom} -\begin{axiom}\label{addition_axiom_2} +\begin{axiom}\label{num_addition_axiom_2} For all $x, y \in \naturals$ $x + \suc{y} = \suc{x} + y = \suc{x+y}$. \end{axiom} -\begin{lemma}\label{naturals_is_equal_to_two_times_naturals} +\begin{lemma}\label{num_naturals_is_equal_to_two_times_naturals} $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$. \end{lemma} -- cgit v1.2.3