diff options
| -rw-r--r-- | library/function.tex | 34 |
1 files changed, 30 insertions, 4 deletions
diff --git a/library/function.tex b/library/function.tex index eb64de2..47d399f 100644 --- a/library/function.tex +++ b/library/function.tex @@ -118,7 +118,7 @@ \end{proof} \begin{definition}\label{funs} - $\funs{A}{B} = \{ f\in\rels{A}{B}\mid \text{$A = \dom{f}$ and $f$ is right-unique}\}$. + $\funs{A}{B} = \{ f\in\rels{A}{B}\mid \text{$A\subseteq \dom{f}$ and $f$ is right-unique}\}$. \end{definition} \begin{abbreviation}\label{function_from_to} @@ -159,7 +159,7 @@ \begin{proposition}\label{funs_elim} Let $f\in\funs{A}{B}$. - Then $f$ is a function to $B$ such that $A = \dom{f}$. + Then $f$ is a function to $B$ such that $A\subseteq \dom{f}$. \end{proposition} \begin{proof} $f$ is a function by \cref{funs_is_function}. % and in particular, a relation. @@ -187,7 +187,8 @@ Then $f(a)\in B$. \end{proposition} \begin{proof} - $(a,f(a)) \in f$ by \cref{funs_elim,function_apply_iff}. + $a\in\dom{f}$ by \cref{funs_elim,subseteq}. + $(a,f(a)) \in f$ by \cref{function_apply_iff}. Thus $f(a)\in B$ by \cref{funs,rels_type_ran}. \end{proof} @@ -197,7 +198,8 @@ Then there exists $b\in B$ such that $(a,b)\in f$. \end{proposition} \begin{proof} - $(a,f(a)) \in f$ by \cref{funs_elim,function_apply_iff}. + $a\in\dom{f}$ by \cref{funs_elim,subseteq}. + $(a,f(a)) \in f$ by \cref{function_apply_iff}. $f(a)\in B$ by \cref{funs_type_apply}. \end{proof} @@ -426,6 +428,20 @@ Follows by \hyperref[setext]{extensionality}. \end{proof} +\begin{proposition}\label{funs_circ} + Let $f\in\funs{A}{B}$. + Let $g\in\funs{B}{C}$. + Then $g\circ f\in\funs{A}{C}$. +\end{proposition} +\begin{proof} + $\dom{f} = A$ by \cref{funs}. + $\dom{g} = B$ by \cref{funs}. + $g$ is composable with $f$. + Omitted. % TODO +\end{proof} + +\subsection{Function restriction} + \begin{proposition}\label{restrl_of_function_is_function} Let $f$ be a function. Let $A$ be a set. @@ -473,6 +489,15 @@ $\inj{A}{B} = \{f\in\funs{A}{B}\mid \text{for all $x,y\in A$ such that $f(x)=f(y)$ we have $x = y$}\}$. \end{definition} +\begin{proposition}\label{inj_circ} + Let $f\in\inj{A}{B}$. + Let $g\in\inj{B}{C}$. + Then $g\circ f\in\surj{A}{C}$. +\end{proposition} +\begin{proof} + Omitted. % TODO +\end{proof} + \subsection{Surjections} \begin{abbreviation}\label{surjection} @@ -596,6 +621,7 @@ \end{proposition} \begin{proof} $g\circ f\in\surj{A}{C}$ by \cref{bijections,surjections_circ}. + $g\circ f$ is an injection. \end{proof} |