test/examples/proofdefinefunction.tex


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

% The builtin "-(-)" notation desugars to "\apply{-}{-}".
% This is just a dummy definition.
\begin{definition}\label{apply}
    $\apply{f}{x} = x$.
\end{definition}

% Dummy definition for the domain
\begin{definition}\label{dom}
    $\dom{f} = f$.
\end{definition}

% Dummy definition for right-uniqueness
\begin{definition}\label{rightunique}
    $f$ is right-unique iff $f=f$.
\end{definition}

% Dummy definition for relations
\begin{definition}\label{relation}
    $f$ is a relation iff $f=f$.
\end{definition}

\begin{proposition}\label{definefunctiontest}
    If $x\in y$, then $x\in y$.
\end{proposition}
\begin{proof}
    Let $f(z) = z$ for $z\in x$.
\end{proof}