Constant function formal definition

Question

A generic function $F : X \rightarrow Y$ can be defined as $\forall x \in X \exists !y \in Y (x, y) \in F$. How about the formal definition of a constant function? The formula $\exists !y \in Y \forall x \in X (x, y) \in F$ does not seem right to me, since it does not prevent that the same element in the set $X$ is mapped to multiple different elements in the set $Y$. Instead, it only prevents that two different constant lines can be mapped from the same set $X$.

Answer 1

How about just combining the two statements together? $$(\forall x\in X\ \exists!y\in Y\ (x,y)\in F)\land(\exists y\in Y\ \forall x\in X\ (x,y)\in F)$$ Note that uniqueness of the $\exists$ in ths second statement is not required: suppose two such $y$'s existed, $y_1$ and $y_2$. Then for any element $x\in X$, $(x,y_1)$ and $(x,y_2)$ are in $F$, which is not allowed by the first statement. Thus only one such $y$ may exist.

Answer 2

The definition $\exists !y \in Y \forall x \in X (x, y) \in F$ does not seem right to me, since it does not prevent that two different elements in the set $X$ are mapped to the same element in the set $Y$.

But you do not want to prevent that different elements from $X$ get mapped to the same element in $Y$. In fact, you want exactly that to happen: different elements get mapped all to the same element in $Y$.

So your definition correctly describes constant functions, if you also require $F$ to be a function. So you could use both axioms and combine them with a $\land$ symbol.

Answer 3

A generic function $F$ mapping set $X$ to set $Y$ can also be defined as follows:

$~~~~~~\forall a\in X: F(a)\in Y~~~~~$ or $~~~~~\forall x: [x\in X \implies F(x)\in Y]$

Then a constant function would be defined as:

$~~~~~~\forall a\in X:F(a)=y_0~~~~~$ or $~~~~~\forall a:[a\in X \implies F(x) = y_0]~~~ $for some $y_0 \in Y$