Proving that a function is 'well-defined'

Question

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

Answer 1

I think your question is confusing (you are confused) , although the essence of your argument is correct. I'll start with the confusion.

The assertion

$$a=b \implies f(a) = f(b)$$

is a literally a tautology because the $=$ on the left says essentially that "$a$" and "$b$" are just two names for the same thing. So it's not what you want to prove. (Also: this choice of notation is confusing since your reader expects something named "$b$" to be an element of $B$, not $A$.)

To show that a relation $f$ is a function you need to show that if $(a,x)$ and $(a,y)$ are in $f$ then $x=y$. Until you show that you can't even make sense of the notation "$f(a)$".

But I don't think that's what you're really asking about. For your $f$ to be "well defined" when its domain is a partition of a set and the definition is in terms of elements of the set you need to check that the value you want to assign does not depend on the choice of the element you use to represent the block of the partition. And that's what you've done.

Answer 2

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.