Suppose I have a relation $f \subset A \times B$. Now, I want to prove that this is a function. Thus, I need to prove:
$\forall a \in A, \exists ! b \in B: f(a) = b$
From what I encountered, the usual procedure is to prove that (if we know that the image will be element of the codomain):
$a = b \Rightarrow f(a) = f(b)$
For example, if we define the following structure,
$+: \mathbb{Z}/n\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z} \rightarrow \mathbb{Z}/n\mathbb{Z}: ([a]_n,[b]_n) \mapsto [a+b]_n$
we must check that the operation does not depend on the chosen representants. Hence, we take $[a_1]_n = [a_2]_n$ and $[b_1]_n = [b_2]_n$, and then we show that $[a_1 + b_1]_n = [a_2 + b_2]_n$ (and this is $a = b \Rightarrow f(a) = f(b)$ in disguised form)
Why is it sufficient to show that $ a= b \Rightarrow f(a) = f(b)$. Can someone deduce this from the definition I wrote above?
Thanks in advance
Best Answer
You abuse notations; $f(a)$ is meaningful only if $f$ is a function. However, we can describe what happens in your example more generally.
Let $\sim$ be a equivalence relation over a set $S$, and $f:S \to X$ be a function. (The domain of $f$ could be other set: e.g. $T\times S$ or $S^n$, but it doesn't matter.) $f$ may not define a function over $S/\sim$, a set of all equivalence classes.
However, if $x\sim y$ then $f(x)=f(y)$, we can define a function $f':(S/\sim) \to X$, by $f'([x]) = f(x)$. The definition does not depend on representatives by our assumption.