From d5b31ee7dc5992687f214d77e795bab53d5fe65d Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Wed, 14 Aug 2024 12:53:47 +0200
Subject: some wishes for NaprocheZF

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

(limited to 'library/wunschzettel.tex')

diff --git a/library/wunschzettel.tex b/library/wunschzettel.tex
new file mode 100644
index 0000000..b2681fd
--- /dev/null
+++ b/library/wunschzettel.tex
@@ -0,0 +1,99 @@
+%This is just a .tex file with a wishlist of functionalitys 
+
+
+Tupel struct
+
+\newtheorem{struct2}[theoremcount]{Struct2}
+
+\begin{theorem}
+    %Some Theorem.
+\end{theorem}
+\begin{proof}
+    %Wish for nice Function definition. --------------------- 
+
+    %Some Proof where we need a Function.
+    %Privisuly defined.
+    $n \in \naturals$.
+    There is a Set $A = \{A_{0}, ..., A_{n}\}$.
+    For all $i$ we have $A_{i} \subseteq X$.
+
+    Define function $f: X \to Y$,
+    \begin{align}
+        &x \mapsto \rfrac{y}{n} &; if \exists k \in \{1, ... n\}. x \in A_{k} \\
+        &x \mapsto 0 &; if x  \phi(x) \\ 
+        %phi is some fol formula
+
+        &x \mapsto \eta &; for \phi(x) and \psi(\eta) 
+
+        &x \mapsto \some_term(x)(u)(v)(w) &; \exist.u,v,w \psi(x)(u)(v)(w) \\ 
+        % here i see the real need of varibles that can be useds in the define term
+
+        &x \mapsto \some_else_term(x)   &; else 
+        % the else term would be great 
+
+        % the following axioms should be automaticly added.
+        % \dom{f} = X
+        % \ran{f} \subseteq Y
+        % f is function
+
+        % therefor we should add the prompt for a proof that f is well defined
+    \end{align}
+    \begin{proof_well_defined}
+        % we need to proof that f allways maps X to Y
+    \end{proof_well_defined}
+
+    % more proof but now i can use the function f
+
+    % --------------------------------------------------------
+
+
+\end{proof}
+
+
+%------------------------------------------
+% My wish for a new struct 
+% I think this could be just get implemented along with the old struct
+
+
+% If take we only take tupels,
+% then just a list of defining fol formulas should be enougth. 
+\begin{struct2}
+    We say $(X,O)$ is a topological space if
+    \begin{enumerate}
+        \item $X$ is a set. % or X = \{...\mid .. \} or X = \naturals ... or ...
+        \item $O \subseteq \pow X$.
+        \item $\forall x,y \in O. x \union y \in O$ 
+        \item %another formula
+        \item %....
+    \end{enumerate} 
+\end{struct2}
+
+
+% Then the proof of some thing is a structure is more easy.
+% Since if we have just a tupel and some formulas which has to be fufilled,
+% then we can make a proof as follows.
+
+\begin{struct2}
+    We say $(A,i,N)$ is a indexed set if
+    \begin{enumerate}
+        \item $f$ is a bijection from $N$ to $A$
+        \item $N \subseteq \naturals$
+    \end{enumerate}
+\end{struct2}
+
+
+\begin{theorem}
+    Let $A = \{ \{n\} \mid n \in \naturals \}$.
+    Let function $f: \naturals \to \pow{\naturals}$ such that,
+    \begin{algin}
+        \item x \mapsto \{x\} ; x \in \naturals
+    \end{algin}
+    Then $(A, f, \naturals)$ is a indexed set.
+\end{theorem}
+\begin{proof}
+    % Then we only need to proof that:
+    % \ran{f} = A
+    % \dom{f} = \naturals
+    % f is a bijection between $\naturals$ to $A$.
+\end{proof}
+
-- 
cgit v1.2.3

