This one is not just in Dummit and Foote; it's just too easy to miss. I'd guess it appears in half the places that state this result. Fixed it in my own lecture notes a few months ago.
I ran into this same thing formalizing some of my old notes in Lean a few days ago. The tricky thing I suppose is that 1. Left invertibility implies injectivity. 2. Surjectivity iff right invertibility, and 3. Surjectivity rules out this corner case, so bijectivity iff invertibility. So this one vacuous case just throws a wrench in what is "supposed" to be true.
It warms my heart every time I see an interactive proof assistant being used to improve rather than simply slow down mathematical thinking.
After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.
That's not actually important to the counter example, it could as easily be A = {1}, B = {1, 2}, f = {(1, 1)}. The shape of the counter example here is that B has more elements than A.
It's also the definitions the book supplies though (and the standard ones). Mathematics works over definitions. Everyone is free to do math over whatever definitions they want - but what is or isn't true follows from them. Lots of definitions and theorems exclude things like empty-set cases because they're weird, but that has to be explicit (otherwise someone will apply a theorem to the empty set and it will lead them to incorrect conclusions).
I mean, yes. But "it doesn't hold that <anything>" is equivalent to "it holds that <not anything>" and since not anything is also anything... Ah, I see.
How does this f satisfy the first criterion, if A is uninhabited? It feels like this function can't be invoked. Am I thinking too much in terms of types here?
When there are no pairs, its certainly true that the first element of each pair comes from A. Just like if there are no living dinosaurs its true that all living dinosaurs speak English.
I was trying to come up with something to explain why I couldn't see it myself: every element of an empty set of integers is both even and odd. This feels counterintuitive to me, until I flip it around into a question: what is the set of all integers that are both even and odd?
I asked AI to formalize an old important paper in analysis. In the paper there is a sequence of epsilon_n > 0, epsilon_n -> 0. It came back, and said: "I formalized it, it is all good, but the assumption that epsilons > 0 is not used anywhere. Shall we remove it, you a get a stronger result this way?"
After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.
https://github.com/ityonemo/bpa
Its painfully verbose and explicit but its designed to let you cut down to the structure of the proof with a query language
It's also the definitions the book supplies though (and the standard ones). Mathematics works over definitions. Everyone is free to do math over whatever definitions they want - but what is or isn't true follows from them. Lots of definitions and theorems exclude things like empty-set cases because they're weird, but that has to be explicit (otherwise someone will apply a theorem to the empty set and it will lead them to incorrect conclusions).
I believe it doesn't make any difference to any meaningful result. It merely makes it easier to write theorems without specifying exceptions.
In other words, the statement "for every x in {} it holds that <anything>" is always true.
The first criterion for a function is stated as:
> The first item in each pair comes from A.
The counter-evidence for the proposition says:
> Let A = {}, and B = {1}. Let f: A -> B = {}
How does this f satisfy the first criterion, if A is uninhabited? It feels like this function can't be invoked. Am I thinking too much in terms of types here?
I was trying to come up with something to explain why I couldn't see it myself: every element of an empty set of integers is both even and odd. This feels counterintuitive to me, until I flip it around into a question: what is the set of all integers that are both even and odd?
LOL