diff options
Diffstat (limited to 'library/function.tex')
| -rw-r--r-- | library/function.tex | 753 |
1 files changed, 753 insertions, 0 deletions
diff --git a/library/function.tex b/library/function.tex new file mode 100644 index 0000000..eb64de2 --- /dev/null +++ b/library/function.tex @@ -0,0 +1,753 @@ +\section{Functions} + +\import{set.tex} +\import{relation.tex} +\import{relation/uniqueness.tex} + + +\begin{abbreviation}\label{function} + $f$ is a function iff $f$ is right-unique and $f$ is a relation. +\end{abbreviation} + +% The builtin "-(-)" notation desugars to "\apply{-}{-}". +\begin{definition}\label{apply} + $\apply{f}{x} = \unions{\img{f}{\{x\}}}$. +\end{definition} + +\begin{proposition}\label{function_rightunique} + Let $f$ be a function. + Suppose $(a,b), (a, b')\in f$. + Then $b = b'$. +\end{proposition} +\begin{proof} + Follows by \hyperref[rightunique]{right-uniqueness}. +\end{proof} + +\begin{proposition}\label{function_apply_intro} + Let $f$ be a function. + Suppose $(a,b)\in f$. + Then $f(a) = b$. +\end{proposition} +\begin{proof} + Let $B = \img{f}{\{a\}}$. + $B = \{b'\in\ran{f}\mid (a,b')\in f \}$ by \cref{img_singleton}. + $b\in\ran{f}$. + For all $b'\in B$ we have $(a, b')\in f$. + For all $b', b''\in B$ we have $b' = b''$ by \hyperref[rightunique]{right-uniqueness}. + Then $B = \{b\}$ by \cref{singleton_iff_inhabited_subsingleton}. + Then $\unions{B} = b$. + Thus $f(a) = b$ by \cref{apply}. +\end{proof} + +\begin{proposition}\label{function_member_elim} + Let $f$ be a function. + Suppose $w\in f$. + Then there exists $x\in\dom{f}$ such that $w = (x, f(x))$. +\end{proposition} +\begin{proof} + Follows by \cref{apply,function_apply_intro,dom,relation}. +\end{proof} + +\begin{proposition}\label{function_apply_elim} + Let $f$ be a function. + Suppose $x\in\dom{f}$. + Then $(x,f(x))\in f$. +\end{proposition} +\begin{proof} + Follows by \cref{dom_iff,function_apply_intro}. +\end{proof} + +\begin{proposition}\label{function_apply_iff} + Let $f$ be a function. + $(a,b)\in f$ iff $a\in\dom{f}$ and $f(a) = b$. +\end{proposition} + +\begin{proposition}\label{fun_subseteq} + Let $f, g$ be functions. + Suppose $\dom{f}\subseteq \dom{g}$. + Suppose for all $x\in\dom{f}$ we have $f(x) = g(x)$. + Then $f\subseteq g$. +\end{proposition} +\begin{proof} + For all $x,y$ such that $(x,y)\in f$ we have $(x,y)\in g$. + Follows by \cref{subseteq,relation}. +\end{proof} + +\begin{proposition}[Function extensionality]\label{funext} + Let $f, g$ be functions. + Suppose $\dom{f} = \dom{g}$. + Suppose for all $x$ we have $f(x) = g(x)$. + Then $f = g$. +\end{proposition} +\begin{proof} + $\dom{f}\subseteq \dom{g}\subseteq \dom{f}$. + For all $x\in\dom{f}$ we have $f(x) = g(x)$. + Thus $f\subseteq g$. + For all $x\in\dom{g}$ we have $f(x) = g(x)$. + Thus $g\subseteq f$. +\end{proof} + +\begin{proposition}\label{fun_ran_iff} + Let $f$ be a function. + $b\in\ran{f}$ iff there exists $a\in\dom{f}$ such that $f(a) = b$. +\end{proposition} +\begin{proof} + Follows by \cref{ran,function_apply_iff}. +\end{proof} + +\begin{abbreviation}\label{function_on} + $f$ is a function on $X$ iff $f$ is a function and $X = \dom{f}$. +\end{abbreviation} + +\begin{abbreviation}\label{function_to} + $f$ is a function to $Y$ iff $f$ is a function and for all $x\in\dom{f}$ we have $f(x)\in Y$. +\end{abbreviation} + +\begin{proposition}\label{function_on_weaken_codom} + Let $f$ be a function to $B$. + Suppose $B\subseteq C$. + Then $f$ is a function to $C$. +\end{proposition} + +\begin{proposition}\label{function_to_ran} + Let $f$ be a function to $B$. + Then $\ran{f}\subseteq B$. +\end{proposition} +\begin{proof} + Follows by \cref{ran,subseteq,apply,function_member_elim,pair_eq_iff,dom}. +\end{proof} + +\begin{definition}\label{funs} + $\funs{A}{B} = \{ f\in\rels{A}{B}\mid \text{$A = \dom{f}$ and $f$ is right-unique}\}$. +\end{definition} + +\begin{abbreviation}\label{function_from_to} + $f$ is a function from $X$ to $Y$ iff $f\in\funs{X}{Y}$. +\end{abbreviation} + +\begin{proposition}\label{funs_is_relation} + Let $f\in\funs{A}{B}$. + Then $f$ is a relation. +\end{proposition} +\begin{proof} + Follows by \cref{funs,rels_is_relation}. +\end{proof} + +\begin{proposition}\label{funs_is_function} + Let $f\in\funs{A}{B}$. + Then $f$ is a function. +\end{proposition} + +\begin{proposition}\label{funs_subseteq_rels} + $\funs{A}{B}\subseteq\rels{A}{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{funs,subseteq}. +\end{proof} + +\begin{proposition}\label{funs_intro} + Let $f$ be a function to $B$ such that $A=\dom{f}$. + Then $f\in\funs{A}{B}$. +\end{proposition} +\begin{proof} + %$f$ is a function. + $\dom{f}\subseteq A$ by \cref{subseteq_refl}. + $\ran{f}\subseteq B$ by \cref{function_to_ran}. + Thus $f\in\rels{A}{B}$ by \cref{rels_intro_dom_and_ran}. + Thus $f\in\funs{A}{B}$ by \cref{funs}. +\end{proof} + +\begin{proposition}\label{funs_elim} + Let $f\in\funs{A}{B}$. + Then $f$ is a function to $B$ such that $A = \dom{f}$. +\end{proposition} +\begin{proof} + $f$ is a function by \cref{funs_is_function}. % and in particular, a relation. + It suffices to show that for all $a\in\dom{f}$ we have $f(a)\in B$ by \cref{funs}. + Fix $a\in\dom{f}$. + Take $b$ such that $f(a) = b$. + Thus $(a,b)\in f$ by \cref{function_apply_elim}. + Now $b\in\ran{f}$ by \cref{ran_iff}. + Finally $\ran{f}\subseteq B$ by \cref{funs,rels_ran_subseteq}. +\end{proof} + +\begin{proposition}\label{funs_weaken_codom} + Let $f\in\funs{A}{B}$. + Suppose $B\subseteq D$. + Then $f\in\funs{A}{D}$. +\end{proposition} +\begin{proof} + $f\in\rels{A}{D}$ by \cref{funs,rels_weaken_codom}. + Follows by \cref{funs}. +\end{proof} + +\begin{proposition}\label{funs_type_apply} + Let $f\in\funs{A}{B}$. + Let $a\in A$. + Then $f(a)\in B$. +\end{proposition} +\begin{proof} + $(a,f(a)) \in f$ by \cref{funs_elim,function_apply_iff}. + Thus $f(a)\in B$ by \cref{funs,rels_type_ran}. +\end{proof} + +\begin{proposition}\label{funs_tuple_intro} + Let $f\in\funs{A}{B}$. + Let $a\in A$. + 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}. + $f(a)\in B$ by \cref{funs_type_apply}. +\end{proof} + + +% LATER techincally ambiguous with the current grammar (as of 2022-04-24) +% but the ambiguity gets resolved during interpretation. +% the options are (probably): +% +% 1: function such that ( ... and for all ...) +% 2: (function such that ...) and for all +% +% \begin{definition} +% $f$ is a function from $X$ to $Y$ iff $f$ is a function such that $\dom{f} = X$ and for all $x\in X$ we have $f(x)\in Y$. +% \end{definition} + +\begin{proposition}\label{funs_ran} + Let $f\in\funs{A}{B}$. + Then $\ran{f}\subseteq B$. +\end{proposition} +\begin{proof} + $f$ is a function to $B$. +\end{proof} + + + +\subsection{Image of a function} + +\begin{proposition}\label{img_of_function_intro} + Let $f$ be a function. + Suppose $x\in\dom{f}\inter X$. + Then $f(x)\in \img{f}{X}$. +\end{proposition} +\begin{proof} + $x\in X$ by \cref{inter_elim_right}. + Thus $(x,f(x))\in f$ by \cref{function_apply_elim,inter_elim_left}. +\end{proof} + +\begin{proposition}\label{img_of_function_elim} + Let $f$ be a function. + Suppose $y\in \img{f}{X}$. + Then there exists $x\in\dom{f}\inter X$ such that $y = f(x)$. +\end{proposition} +\begin{proof} + Take $x\in X$ such that $(x,y)\in f$. + Then $x\in\dom{f}$ and $y = f(x)$ by \cref{dom_intro,function_apply_iff}. +\end{proof} + +\begin{proposition}\label{img_of_function} + Suppose $f$ is a function. + $\img{f}{X} = \{ f(x) \mid x\in\dom{f}\inter X\}$. +\end{proposition} +\begin{proof} + Follows by \cref{img_of_function_intro,img_of_function_elim}. +\end{proof} + +\subsection{Families of functions} + +\begin{abbreviation}\label{family_of_functions} + $F$ is a family of functions iff + every element of $F$ is a function. +\end{abbreviation} + +\begin{proposition}\label{unions_of_compatible_family_of_function_is_function} + Let $F$ be a family of functions. + Suppose that for all $f,g \in F$ we have $f\subseteq g$ or $g\subseteq f$. + Then $\unions{F}$ is a function. +\end{proposition} +\begin{proof} + $\unions{F}$ is a relation by \cref{unions_of_family_of_relations_is_relation}. + For all $x,y, y'$ such that $(x,y),(x,y')\in \unions{F}$ + there exists $f\in F$ such that $(x,y),(x,y')\in f$ + by \cref{unions_iff,subseteq}. + %Hence for all $x,y, y'$ such that $(x,y),(x,y')\in \unions{F}$ we have $y = y'$ + % by \cref{rightunique}. + Thus $\unions{F}$ is right-unique by \cref{rightunique}. +\end{proof} + + +\subsection{The empty function} + +\begin{proposition}\label{emptyset_is_function} + $\emptyset$ is a function. +\end{proposition} +%\begin{proof} +% For all $x,y, y'$ we have +% if $(x,y),(x,y')\in \emptyset$, then $y = y'$. +%\end{proof} + +\begin{proposition}\label{emptyset_is_function_on_emptyset} + $\emptyset$ is a function on $\emptyset$. +\end{proposition} + +\begin{proposition}\label{codom_of_emptyset_can_be_anything} + $\emptyset$ is a function to $X$. +\end{proposition} + +\begin{proposition}\label{emptyset_is_injective} + $\emptyset$ is injective. +\end{proposition} +% LATER filter throws out the definition of injective, smh + + +\subsection{Function composition} + +\begin{abbreviation}\label{composable} + $g$ is composable with $f$ iff $\ran{f}\subseteq \dom{g}$. +\end{abbreviation} + +\begin{proposition}\label{function_circ} + Suppose $f$ and $g$ are right-unique. + Then $g\circ f$ is a function. +\end{proposition} + +\begin{proposition}\label{circ_apply} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + Let $x\in\dom{f}$. + Then $(g\circ f)(x) = g(f(x))$. +\end{proposition} +\begin{proof} + $(x, g(f(x)))\in g\circ f$ by \cref{circ,ran,subseteq,function_apply_elim}. + $g\circ f$ is a function by \cref{function_circ}. + Thus $(g\circ f)(x) = g(f(x))$ by \cref{function_apply_intro}. +\end{proof} + +\begin{proposition}\label{dom_of_circ} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + $\dom{g\circ f} = \preimg{f}{\dom{g}}$. +\end{proposition} +\begin{proof} + Every element of $\dom{g\circ f}$ is an element of $\preimg{f}{\dom{g}}$ + by \cref{preimg,circ,dom,pair_eq_iff}. + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{dom_circ_exact} + Let $f, g$ be functions. + Suppose $\ran{f} = \dom{g}$. + $\dom{g\circ f} = \dom{f}$. +\end{proposition} +\begin{proof} + Every element of $\dom{g\circ f}$ is an element of $\dom{f}$. + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{ran_of_circ_intro} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + Suppose $y\in \img{g}{\ran{f}}$. + Then $y\in \ran{g\circ f}$. +\end{proposition} +\begin{proof} + Take $x\in\ran{f}$ such that $(x, y)\in g$. + Take $x'\in\dom{f}$ such that $(x', x)\in f$. + Then $(x', y) \in g\circ f$. + Follows by \cref{ran_intro}. +\end{proof} + +\begin{proposition}\label{ran_of_circ_elim} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + Suppose $y\in \ran{g\circ f}$. + Then $y\in \img{g}{\ran{f}}$. +\end{proposition} +\begin{proof} + Take $x\in\dom{f}$ such that $(x, y)\in g\circ f$ + by \cref{circ,circ_iff,ran,dom}. + $f(x)\in\ran{f}$. + $(f(x), y)\in g$ + by \cref{function_apply_intro,apply,circ_iff}. + Follows by \cref{img_iff}. +\end{proof} + +\begin{proposition}\label{ran_of_circ} + Let $f, g$ be functions. + Suppose $g$ is composable with $f$. + Then $\ran{g\circ f} = \img{g}{\ran{f}}$. +\end{proposition} +\begin{proof} + Follows by set extensionality. +\end{proof} + +\begin{proposition}\label{ran_circ_exact} + Let $f, g$ be functions. + Suppose $\ran{f} = \dom{g}$. + Then $\ran{g\circ f} = \ran{g}$. +\end{proposition} +\begin{proof} + \begin{align*} + \ran{g\circ f} + &= \img{g}{\ran{f}} + \explanation{by \cref{subseteq_refl,ran_of_circ}}\\ + &= \img{g}{\dom{g}} + \\ % by assumption + &= \ran{g} + \explanation{by \cref{img_dom}} + \end{align*} +\end{proof} + + +\begin{proposition}\label{img_of_circ_elim} + Let $f, g$ be functions. + Let $A$ be a set. + Suppose $\ran{f}\subseteq \dom{g}$. + Suppose $c\in\img{g\circ f}{A}$. + Then $c\in\img{g}{\img{f}{A}}$. +\end{proposition} +\begin{proof} + Take $a\in A$ such that $(a,c)\in g\circ f$. + Take $b$ such that $(a,b)\in f$ and $(b, c)\in g$. + Then $b\in\img{f}{A}$. + Follows by \cref{img_iff}. +\end{proof} + +\begin{proposition}\label{img_of_circ} + Let $f, g$ be functions. + Let $A$ be a set. + Suppose $\ran{f}\subseteq\dom{g}$. + Then $\img{g\circ f}{A} = \img{g}{\img{f}{A}}$. +\end{proposition} +\begin{proof} + For all $c$ we have $c\in\img{g}{\img{f}{A}}$ + iff $c\in\img{g\circ f}{A}$ + by \cref{circ_iff,img_iff}. + Follows by \hyperref[setext]{extensionality}. +\end{proof} + +\begin{proposition}\label{restrl_of_function_is_function} + Let $f$ be a function. + Let $A$ be a set. + $\restrl{f}{A}$ is a function. +\end{proposition} + +\begin{proposition}\label{restrl_of_function_apply} + Let $f$ be a function. + Suppose $A\subseteq\dom{f}$. + Let $a\in A$. + Then $(\restrl{f}{A})(a) = f(a)$. +\end{proposition} +\begin{proof} + Then $(a,f(a))\in f$. + Then $(a,f(a))\in \restrl{f}{A}$ by \cref{restrl_iff}. + Thus $(\restrl{f}{A})(a) = f(a)$. +\end{proof} + +\begin{proposition}\label{function_apply_default} + Suppose $x\notin\dom{f}$. + Then $f(x) = \emptyset$. +\end{proposition} +\begin{proof} + $\img{f}{\{x\}} = \emptyset$ by \cref{setext,notin_emptyset,img_singleton_iff,dom_intro}. + Follows by \cref{apply,unions_emptyset}. +\end{proof} + + + +\subsection{Injections} + +\begin{proposition}\label{injective_function} + Suppose $f$ is a function. + $f$ is injective iff for all $x,y\in\dom{f}$ we have $f(x) = f(y) \implies x = y$. +\end{proposition} +\begin{proof} + Follows by \cref{injective,function_apply_iff}. +\end{proof} + +\begin{abbreviation}\label{injection} + $f$ is an injection iff $f$ is an injective function. +\end{abbreviation} + +\begin{definition}\label{inj} + $\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} + +\subsection{Surjections} + +\begin{abbreviation}\label{surjection} + $f$ is a surjection onto $Y$ iff $f$ is a function such that $f$ is surjective on $Y$. +\end{abbreviation} + +\begin{definition}\label{surj} + $\surj{A}{B} = \{f\in\funs{A}{B}\mid \text{for all $b\in B$ there exists $a\in A$ such that $f(a) = b$}\}$. +\end{definition} + +\begin{abbreviation}\label{surjection_from_to} + $f$ is a surjection from $A$ to $B$ iff $f\in\surj{A}{B}$. +\end{abbreviation} + +\begin{lemma}\label{surjection_ran} + Let $f$ be a function. + Then $f$ is surjective on $\ran{f}$. +\end{lemma} +\begin{proof} + It suffices to show that for all $y\in\ran{f}$ there exists $x\in\dom{f}$ such that $f(x) = y$. + Fix $y\in\ran{f}$. + Take $x$ such that $(x,y)\in f$. + Then $x\in\dom{f}$ and $f(x) = y$ by \cref{dom,function_apply_iff}. +\end{proof} + +\begin{lemma}\label{surj_to_fun} + Let $f\in\surj{A}{B}$. + Then $f\in\funs{A}{B}$. +\end{lemma} + +\begin{lemma}\label{fun_to_surj} + Let $f\in\funs{A}{B}$. + Then $f\in\surj{A}{\ran{f}}$. +\end{lemma} +\begin{proof} + $f\in\rels{A}{\ran{f}}$ by \cref{funs,rels_restrict_ran}. + Thus $f\in\funs{A}{\ran{f}}$ by \cref{funs}. + It suffices to show that for all $b\in\ran{f}$ there exists $a\in A$ such that $f(a) = b$ by \cref{surj}. + Fix $b\in\ran{f}$. + Take $a$ such that $(a,b)\in f$. + Thus $f(a)=b$ by \cref{function_apply_iff,funs_elim}. + We have $a\in\dom{f} = A$. + Follows by assumption. +\end{proof} + +\begin{corollary}\label{ran_of_surj} + Let $f\in\surj{A}{B}$. + Then $\ran{f} = B$. +\end{corollary} +\begin{proof} + % TODO clean + We have $f$ is a function by \cref{surj,funs_is_function}. + Now $\ran{f}\subseteq B$ by \cref{surj,funs_ran}. + It suffices to show that every element of $B$ is an element of $\ran{f}$. + It suffices to show that for all $b\in B$ + there exists $a\in\dom{f}$ such that $f(a) = b$ by \cref{fun_ran_iff}. + Fix $b\in B$. + Take $a\in A$ such that $f(a) = b$ by \cref{surj}. + Then $\dom{f} = A$ by \cref{surj,funs_elim}. +\end{proof} + +\begin{corollary}\label{funs_surj_iff} + Let $f\in\funs{A}{B}$. + Then $f\in\surj{A}{B}$ iff $\ran{f} = B$. +\end{corollary} +\begin{proof} + Follows by \cref{surj,fun_to_surj,ran_of_surj}. +\end{proof} + +\begin{proposition}\label{surjections_circ} + Let $f\in\surj{A}{B}$. + Let $g\in\surj{B}{C}$. + Then $g\circ f\in\surj{A}{C}$. +\end{proposition} +\begin{proof} + $\dom{f} = A$ by \cref{surj,funs}. + $\dom{g} = B = \ran{f}$ by \cref{surj,funs,ran_of_surj}. + $\dom{g\circ f} = A$ by \cref{surj_to_fun,funs_is_function,dom_circ_exact}. + Omitted. % TODO +\end{proof} + + + +\subsection{Bijections} + +\begin{definition}\label{bijections} + $\bijections{A}{B} = \{ f\in\surj{A}{B} \mid \text{$f$ is injective}\}$. +\end{definition} + +\begin{abbreviation}\label{bijection} + $f$ is a bijection from $A$ to $B$ iff $f\in\bijections{A}{B}$. +\end{abbreviation} + +\begin{proposition}\label{bijections_to_funs} + Every element of $\bijections{A}{B}$ is an element of $\funs{A}{B}$. +\end{proposition} +\begin{proof} + Follows by \cref{bijections,surj}. +\end{proof} + +\begin{proposition}\label{bijection_is_function} + Every element of $\bijections{A}{B}$ is a function. +\end{proposition} +\begin{proof} + Follows by \cref{bijections_to_funs,funs_is_function}. +\end{proof} + +\begin{proposition}\label{bijections_dom} + Let $f\in\bijections{A}{B}$. + Then $\dom{f} = A$. +\end{proposition} +\begin{proof} + $f\in\funs{A}{B}$ by \cref{bijections_to_funs}. + Follows by \cref{funs}. +\end{proof} + +\begin{proposition}\label{bijection_circ} + Let $f$ be a bijection from $A$ to $B$. + Let $g$ be a bijection from $B$ to $C$. + Then $g\circ f$ is a bijection from $A$ to $C$. +\end{proposition} +\begin{proof} + $g\circ f\in\surj{A}{C}$ by \cref{bijections,surjections_circ}. + $g\circ f$ is an injection. +\end{proof} + +\subsection{Converse as a function} + +\begin{proposition}\label{converse_of_function_is_injective} + Let $f$ be a function. + Then $\converse{f}$ is injective. % i.e. an injective relation. +\end{proposition} + +\begin{proposition}\label{injective_converse_is_function} + Suppose $f$ is injective. % NOTE: f need not be a function! + Then $\converse{f}$ is a function. +\end{proposition} + +\begin{proposition}\label{bijective_converse_is_function} + Let $f$ be a bijection from $A$ to $B$. + Then $\converse{f}$ is a function. +\end{proposition} +\begin{proof} + Follows by \cref{bijections,injective_converse_is_function}. +\end{proof} + +\begin{proposition}\label{bijective_converse_are_funs} + Let $f$ be a bijection from $A$ to $B$. + Then $\converse{f}\in\funs{B}{A}$. +\end{proposition} +\begin{proof} + %\begin{align*} + % \dom{\converse{f}} + % &= \ran{f} + % \explanation{by \cref{dom_converse}}\\ + % &= B + % \explanation{by \cref{ran_of_surj}} + %\end{align*} + $\dom{\converse{f}} = \ran{f} = B$ by \cref{bijections,dom_converse,ran_of_surj}. + Omitted. % TODO +\end{proof} + +\begin{proposition}\label{bijective_converse_are_surjs} + Let $f$ be a bijection from $A$ to $B$. + Then $\converse{f}\in\surj{B}{A}$. +\end{proposition} +\begin{proof} + We have $\converse{f}\in\funs{B}{A}$ by \cref{bijective_converse_are_funs}. + It suffices to show that $\ran{\converse{f}} = A$ by \cref{funs_surj_iff}. + We have $\dom{f} = A$ by \cref{bijections_dom}. + Thus $\ran{\converse{f}} = A$ by \cref{ran_converse}. +\end{proof} + +\begin{proposition}\label{bijection_converse_is_bijection} + Let $f$ be a bijection from $A$ to $B$. + Then $\converse{f}$ is a bijection from $B$ to $A$. +\end{proposition} +\begin{proof} + $\converse{f}\in\funs{B}{A}$ by \cref{bijective_converse_are_funs}. + $\converse{f}$ is injective by \cref{bijection_is_function,converse_of_function_is_injective}. + $\converse{f}\in\surj{B}{A}$ by \cref{bijective_converse_are_surjs}. + Follows by \cref{bijections}. +\end{proof} + +\subsubsection{Inverses of a function} + +\begin{abbreviation}\label{leftinverse} + $g$ is a left inverse of $f$ iff for all $x\in\dom{f}$ we have $g(f(x)) = x$. +\end{abbreviation} + +% This definition of right inverse is probably not particularly useful... +\begin{abbreviation}\label{rightinverse} + $g$ is a right inverse of $f$ iff $f\circ g = \identity{\dom{g}}$. +\end{abbreviation} + +\begin{abbreviation}\label{rightinverseon} + $g$ is a right inverse of $f$ on $B$ iff $f\circ g = \identity{B}$. +\end{abbreviation} + +\begin{proposition}\label{injective_converse_is_leftinverse} + Let $f$ be an injection. + Then $\converse{f}$ is a left inverse of $f$. +\end{proposition} +\begin{proof} + $\converse{f}$ is a function by \cref{injective_converse_is_function}. + + Omitted. % TODO +\end{proof} + + + +\subsection{Identity function} + +\begin{proposition}\label{id_rightunique} + $\identity{A}$ is right-unique. +\end{proposition} +\begin{proof} + Follows by \cref{id,rightunique,pair_eq_iff}. +\end{proof} + +\begin{proposition}\label{id_is_function} + $\identity{A}$ is a function. +\end{proposition} + +\begin{proposition}\label{id_is_function_on} + $\identity{A}$ is a function on $A$. +\end{proposition} + +\begin{proposition}\label{id_is_function_to} + $\identity{A}$ is a function to $A$. +\end{proposition} + +\begin{proposition}\label{id_is_function_from_to} + $\identity{A}$ is a function from $A$ to $A$. +\end{proposition} +\begin{proof} + $\identity{A}\in\rels{A}{A}$ by \cref{id_elem_rels}. + Follows by \cref{funs,id_is_function_on,id_is_function_to}. +\end{proof} + +\begin{proposition}\label{id_apply} + Suppose $a\in A$. + % TODO/FIXME fix grammar, then simplify + %Then $\identity{A}(a) = a$. + Suppose $f = \identity{A}$. + Then $f(a) = a$. +\end{proposition} +\begin{proof} + $(a,a)\in\identity{A}$ by \cref{id_iff}. + Follows by \cref{id_is_function,function_apply_intro}. +\end{proof} + +\begin{proposition}\label{id_elem_funs} + $\identity{A}\in\funs{A}{A}$. +\end{proposition} +\begin{proof} + $\identity{A}$ is a function. + $\identity{A}\in\rels{A}{A}$. + $\dom{\identity{A}}\subseteq A$. +\end{proof} + + +\begin{proposition}\label{id_elem_surjections} + $\identity{A}\in\surj{A}{A}$. +\end{proposition} +\begin{proof} + We have $\identity{A}\in\funs{A}{A}$ by \cref{id_elem_funs}. + Omitted. % TODO +\end{proof} + +\begin{proposition}\label{id_elem_bijections} + $\identity{A}\in\bijections{A}{A}$. +\end{proposition} +\begin{proof} + $\identity{A}\in\surj{A}{A}$ by \cref{id_elem_surjections}. + $\identity{A}$ is injective by \cref{identity_injective}. + Follows by \cref{bijections}. +\end{proof} |