1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
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}
|
