I don't really know what you just wrote, but it's not "F is a surjection", which is what the post is capturing. If you're not quantifying somehow, even implicit

I don't really know what you just wrote, but it's not "F is a surjection", which is what the post is capturing. If you're not quantifying somehow, even implicitly, then you're just not giving the same definition. It can be written with fewer symbols: `f: [N]->[N] s.t. x != y => f(x) != f(y)` is an equivalent formulation, for instance (since f from a finite set to itself is surjective iff it is bijective iff it is injective). The quantification is now implicit in the "implies" symbol. Not sure how standard `[n]` is to refer to {1,2,…,n}; it was used commonly in my undergrad courses.