A relation $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ is functional if, for each $a\in A$, the set $R\webleft (a\webright )$ is either empty or a singleton.
10.1.1 Functional Relations
Let $A$ and $B$ be sets.
Let $R\colon A\mathrel {\rightarrow \kern -9.5pt\mathrlap {|}\kern 6pt}B$ be a relation.
Proof of Proposition 10.1.1.1.2.
Item 1: Characterisations
We claim that Item 1a and Item 1b are indeed equivalent:
-
•
Item 1a$\implies $Item 1b: Let $\webleft (b,b'\webright )\in B\times B$. We need to show that
\[ \webleft [R\mathbin {\diamond }R^{\dagger }\webright ]\webleft (b,b'\webright )\preceq _{\{ \mathsf{t},\mathsf{f}\} }\chi _{B}\webleft (b,b'\webright ), \]i.e. that if there exists some $a\in A$ such that $b\sim _{R^{\dagger }}a$ and $a\sim _{R}b'$, then $b=b'$. But since $b\sim _{R^{\dagger }}a$ is the same as $a\sim _{R}b$, we have both $a\sim _{R}b$ and $a\sim _{R}b'$ at the same time, which implies $b=b'$ since $R$ is functional.
-
•
Item 1b$\implies $Item 1a: Suppose that we have $a\sim _{R}b$ and $a\sim _{R}b'$ for $b,b'\in B$. We claim that $b=b'$:
-
•
Since $a\sim _{R}b$, we have $b\sim _{R^{\dagger }}a$.
-
•
Since $R\mathbin {\diamond }R^{\dagger }\subset \chi _{B}$, we have
\[ \webleft [R\mathbin {\diamond }R^{\dagger }\webright ]\webleft (b,b'\webright )\preceq _{\{ \mathsf{t},\mathsf{f}\} }\chi _{B}\webleft (b,b'\webright ), \]and since $b\sim _{R^{\dagger }}a$ and $a\sim _{R}b'$, it follows that $\webleft [R\mathbin {\diamond }R^{\dagger }\webright ]\webleft (b,b'\webright )=\mathsf{true}$, and thus $\chi _{B}\webleft (b,b'\webright )=\mathsf{true}$ as well, i.e. $b=b'$.
-
•
This finishes the proof.
