%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}