How do I prove that a function is well defined?

How do you in general prove that a function is well-defined?

$$f:X\to Y:x\mapsto f(x)$$

I learned that I need to prove that every point has exactly one image. Does that mean that I need to prove the following two things:

  1. Every element in the domain maps to an element in the codomain:
    $$x\in X \implies f(x)\in Y$$
  2. The same element in the domain maps to the same element in the codomain: $$x=y\implies f(x)=f(y)$$

At the moment I'm trying to prove this function is well-defined: $$f:(\Bbb Z/12\mathbb Z)^∗→(\Bbb Z/4\Bbb Z)^∗:[x]_{12}↦[x]_4 ,$$ but I'm more interested in the general procedure.


When we write $f\colon X\to Y$ we say three things:

  1. $f\subseteq X\times Y$.
  2. The domain of $f$ is $X$.
  3. Whenever $\langle x,y_1\rangle,\langle x,y_2\rangle\in f$ then $y_1=y_2$. In this case whenever $\langle x,y\rangle\in f$ we denote $y$ by $f(x)$.

So to say that something is well-defined is to say that all three things are true. If we know some of these we only need to verify the rest, for example if we know that $f$ has the third property (so it is a function) we need to verify its domain is $X$ and the range is a subset of $Y$. If we know those things we need to verify the third condition.

But, and that's important, if we do not know that $f$ satisfies the third condition we cannot write $f(x)$ because that term assumes that there is a unique definition for that element of $Y$.


Okay, I'm trying to answer my own question here. This is how a function is defined in "Reading, Writing, and Proving: A Closer Look at Mathematics".

Recall that a relation $f$ from $X$ to $Y$ is a subset of $X\times Y$, and therefore the elements of $f$ are ordered pairs $(x,y)$.

A function $f:X\to Y$ is a relation $f$ from $X$ to $Y$ satisfying:
i). $\forall x\in X ,\exists y\in Y :(x,y)\in f $
ii). $\forall x\in X,\forall y_1,y_2 \in Y : (x,y_1),(x,y_2)\in f\implies y_1=y_2$

An function is often called an map or a mapping. The set is $X$ is called the domain and denoted by $\text{dom}(f)$, and the set $Y$ is called the codomain and denoted by $\text{cod}(f)$. When we know what these two sets are and the two conditions are satisfied, we say that $f$ is a well defined function.

Condition i) makes sure that each element in $X$ is related to some element of $Y$, while condition ii) makes sure that no element in $X$ is related to more than one element of $Y$. Note that it may be the case that an element of $Y$ has no element in $X$ to which it is related; or an element of $Y$ could be related to more than one element of $X$.

Therefore, like Asaf Karagila mentioned, if you want to prove that $f$ is a well defined funciton, and the domain $X$ and codomain $Y$ are given, then you need to show that:

  1. $f$ is a relation from $X$ to $Y$
    $f\subseteq X\times Y$

  2. The domain of $f$ is $X$, every element in $X$ is related to some element of $Y$ $\forall x\in X ,\exists y\in Y :(x,y)\in f $

  3. No element of $X$ is related to more than one element of $Y$ $\forall x\in X,\forall y_1,y_2 \in Y : (x,y_1),(x,y_2)\in f\implies y_1=y_2$


The issue here is that $[x]_{12}$ means an equivalence class of elements of $\def\Z{\mathbb Z}\Z$, specifically the class of all $y$ such that $x-y$ is a multiple of 12. You have some procedure that says you are given one of these equivalence classes, $[x]_{12}$, and you are calculating a value by selecting a representative element, say $y$, from $[x]_{12}$, and then doing something to that representative to get the answer, in this case the object $[y]_4$. But this does not make sense—it is not "well defined"—if the value you get for the given class $[x]_{12}$ depends on which representative $y$ you selected from $[x]_{12}$.

So your job here is to show that the result you get does not depend on which $y$ you pick as a representative of $[x]_{12}$.

As a counterexample, let's consider the "function" that says that $f\left(\frac ab\right) = a+ b$. So for example $f\left(\frac 12\right) = 3$, simple. But no, wait. $\frac12$ is actually an equivalence class; it is the class $\left[\frac12\right]_\mathbb Q$, which contains not only $\frac12$ but also $\frac24$, $\frac36$, and $\frac{576}{288}$. And with the definition given, the value of $f$ does depend on which representative of $\left[\frac12\right]_\mathbb Q$ you chose. $\frac12 = \frac 24$, but if you use $\frac24$ to calculate $f\left(\frac 12\right)$ you get 6 instead of 3. So this is not a well-defined function; it's not a function at all.

In your example you need to show that if you are given a class, say $[x]_{12}$, and you select an element $y$ from it (which could be any integer at all, as long as $y-x\equiv 0\pmod{12}$), and then you consider the equivalence class $[y]_4$, the class you get does not depend on which $y$ you chose from $[x]_{12}$. If it does, then this $f$ operation is an meaningless as the one in the previous paragraph that claimed to have $f\left(\frac ab\right) = a+b$.


You're trying to prove $$f:(\Bbb{Z}/12\Bbb{Z})^*\to(\Bbb{Z}/4\Bbb{Z})^*:[x]_{12}\mapsto[x]_4$$

So, you have to prove that this rule of assignment doesn't depend on the representative of the equivalence class. That is $$[x]_{12}=[y]_{12} \implies [x]_{4}=[y]_{4}$$

For example $[16]_{12}=[4]_{12}$ then $[16]_{4}=[4]_{4}$.

You also need to prove that $$ [x]_{12} \in (\Bbb{Z}/12\Bbb{Z})^* \implies [x]_{4} \in (\Bbb{Z}/4\Bbb{Z})^* $$


An option would be to resort to Relational Algebra, in a pointfree style.
A logic of relations was first proposed by Augustus de Morgan, in 1867.

Functions are just special cases of Relations (binary relations, for that matter).

Given types $A$ and $B$, we denote a relation $R$, from $A$ to $B$, as $B \xleftarrow{R} A$.
We write $b \, R \, a$, to denote $(b,a) \in R$.
In the particular case of functions, for a function $f$, writing $b \, f \, a$ simply means $b = f \, a$, since we expect $b$ to be unique.

Therefore, $b \, R \, a$ is a generalization of $b \, f \, a$.
This generalization applies in many ways. For instance, equality on functions, $f=g$, generalizes to inclusion on relations, $R \subseteq S$, meaning $R$ is (at most) $S$.

Besides inclusion, an important concept to have in mind is the converse of a relation.
The converse of $R$, $B \xleftarrow{R} A$, is $R^\circ$, $A \xleftarrow{R^\circ} B$ (just turn the arrows the other way around).

The converse of a function always exists, as a relation (sometimes, in special cases, as a function too).

Function composition, $f \cdot g$, also generalizes to relations, $R \cdot S$, in the same way.

So, what is it that really defines when a given relation is a function?$\vphantom{Some commands added; A.K.}\newcommand{\img}{\operatorname{img}}\newcommand{\id}{\mathrm{id}}$

Let's look at a special function, $\id$.
We have $b \, \id \, a \equiv b = a$. Not too hard.

Why does $id$ matter?

  • $R$ is reflexive iff $\id \subseteq R$.
  • $R$ is coreflexive iff $R \subseteq \id$.

We then define:

  • Kernel of $R$ as $\ker R \doteq R^\circ \cdot R$.
  • Image of $R$ as $\img R \doteq R \cdot R^\circ$.

Finally, we have the following facts:

  • $\ker R$ is reflexive $\equiv$ $R$ is entire.
  • $\ker R$ is coreflexive $\equiv$ $R$ is injective.
  • $\img R$ is reflexive $\equiv$ $R$ is surjective.
  • $\img R$ is coreflexive $\equiv$ $R$ is simple.

We say relation $f$ is a function iff $f$ is entire and $f$ is simple.
Put in another way, what you want to prove is:

  • $\id \subseteq ker f$ (simplifies to $\id \subseteq f^\circ \cdot f$)
  • $\img f \subseteq \id$ (simplifies to $f \cdot f^\circ \subseteq \id$)

Bonus facts:

  • $\ker (R^\circ) = \img R$
  • $\img (R^\circ) = \ker R$