Is the following logical notation valid in describing the condition for a function $f$ being surjective? If $f: A \rightarrow B$ is a function, then $f$ is surjective if
$$\forall y, \exists x \in A \, : \, y \in B \implies y=f(x)$$
I think it is valid, because it seems equivalent to the traditional definition of surjection where the implication is implicit in the definition.
On
Yes, it's valid. It's equivalent to the usual definition:
$$ \text{$f: A \rightarrow B$ is a surjection} \iff \forall y \in B, \exists x \in A : y = f(x) $$
Anytime you have
"$\forall y, y \in S \implies \text{something about $y$}$"
it's the same as
"$\forall y \in S, \text{something about $y$}$"
I think that one may be defined in terms of the other, deep down in the bowels of whatever set theory you're using.
On
Yes, it is equivalent (edit if you assume that $A$ is not empty, as Rob Arthan pointed out) although someone could complain on the fact it would be more natural to write it as $$\forall y (y \in B \Rightarrow \exists x (x \in A \land f(x)=y))$$
The difference is psycological more than logical and stands in the fact that your form becomes in natural language: for each $y$ there is an $x \in A$ such that
The form I wrote above instead becomes (in natural language): for all $y$ if $y \in B$ then there is an $x \in A$ such that $y=f(x)$.
P.s.: Now I'm wondering on whether these two formulas are equivalent in construtive mathematics.
If $A = B = \emptyset$, the empty function $f = \emptyset \subseteq A \times B$ is a surjection of $A$ onto $B$, but your formula:
$$\forall y \exists x \in A (y \in B \implies y=f(x))$$
which means
$$\forall y \exists x (x \in A \land (y \in B \implies y=f(x)))$$
is false in that case. You need to say:
$$\forall y (y \in B \implies (\exists x \in A (y=f(x))))$$
which is equivalent to the short-hand form:
$$\forall y \in B \exists x \in A (y=f(x))$$
(which is what I think you had in mind when you referred to the "traditional definition" with implicit implications).