On notation: is it better to say $A^B = \{f| f:B \to A\}$ or $A^B = \{f :B \to A| f \text{ is a function}\}$

Question

The title says it all, let $A^B$ denote the set of all functions from $B$ to $A$, then it is better to write in set notation

$A^B = \{f\mid f:B \to A\}$ or $A^B = \{f :B \to A\mid f \text{ is a function}\}$

Answer 1

Let me expand on Dave L. Renfron's answer:

While all notations listed thus far are commonly used and I don't think there is anything wrong with it, there is a reason why $$ A^{B} = \{ f \in \mathcal P(B \times A) \mid f \text{ is a function} \} $$ is preferable. At least until one is comfortable with these notations and there is no fear that these semi-formal notations lead to any problems.

So, let's look at $$ \{ f \mid f \colon B \to A \} $$ again. This can be written equivalently as $$ \{ f \mid f \subseteq B \times A \wedge \forall b \in B \exists a \in A \forall \tilde{a} \in A \colon (b,a) \in f \wedge (b, \tilde{a}) \in f \rightarrow a = \tilde{a} \}. $$ This is pretty unreadable... However, the whole $f \subseteq B \times A \wedge \ldots$ part is simply a formula $\phi$ with $f$ as it's unique free variable. So, fixing $\phi$ as this formula, we have $$ A^B = \{f \mid \phi(f) \}. $$ This problem is, that one may now wrongfully think that this is a legitimate way to define sets. I.e. one might think that for any formula $\psi$ with a unique free variable $x$ $$ \{x \mid \psi(x) \} $$ is a set. However, if we take for example $\psi(x) \equiv x \not \in x$, then $$ \{ x \mid \psi(x) \} = \{x \mid x \not \in x \} $$ is not a set (see Russel's paradox). However, given any set $X$ and any well-formed formula $\psi$ with a unique free variable $x$ ($\psi$ may contain parameters, e.g. our $\phi$ above contained $A$ and $B$ as parameters) $$ \{ x \in X \mid \psi(x) \} $$ is a set. (This is the axiom of separation.)

Hence, if we write $$ A^B = \{f \in \mathcal P(B \times A) \mid f \text{ is a function}\} $$ it immediatly follows that $A^B$ is a set and we don't have to worry that we may have defined something weird. (*)

---

(*) Assuming that your background theory is something like $\operatorname{ZF}$ and consistent, but you shouldn't worry about this last remark. I only included it to be formally correct.

Answer 2

The notation $f:B\to A$ is typically used to denote that $f$ is a function from $B$ into $A$. Thus, saying $$A^B = \{f :B \to A| f \text{ is a function}\}$$ is like saying $A^B$ is the set of all functions $f:B\to A$ such that $f$ is a function. So there is some redundancy.

I, personally, would go with the first option, however your intentions seem clear using either notation.

Answer 3

Perhaps better still is

$$A^B = \{f \in {\mathcal P}(B \times A) \mid f \text{ is a function}\},$$

because this fits the more formal way of defining sets using the Axiom schema of specification (i.e. set builder notation in school math).