CounterexampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The empty set is at most countable but no function from $N$ is onto it

Statement refuted

Refuted claim: every at most countable set is a surjective image of $N$ .

The witness is $\emptyset$ , which is finite, hence at most countable (Finite, countably infinite, countable, uncountable); but there is no function $N \to \emptyset$ at all (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain). So the hypothesis $A \neq \emptyset$ cannot be dropped from the forward direction of A nonempty set is at most countable iff it is a surjective image of $N$ : $\emptyset$ is at most countable, yet it has no surjection from $N$ (Equinumerous sets, $A \approx B$ and $A ⪯ B$ , Injection, surjection, bijection).

Facts & Assumptions

Given: The empty set $\emptyset$ (There is exactly one set with no elements, written $\emptyset$ ) and the naturals $N$ with $0 = \emptyset$ (The natural numbers $N$ (von Neumann)).

[F1]

$A$ is finite when $A \approx n$ for some $n \in N$ ; $0 = \emptyset$ , so $A \approx 0$ holds exactly when $A = \emptyset$ ; and finite sets are at most countable (Finite, countably infinite, countable, uncountable, The natural numbers $N$ (von Neumann), Equinumerous sets, $A \approx B$ and $A ⪯ B$ ).

[F2]

A function from $X$ to $Y$ is a set $f$ of ordered pairs with $dom f = X$ and $ran f \subseteq Y$ ; equivalently $f \subseteq X \times Y$ with $dom f = X$ (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, The Cartesian product $A \times B : = {z \in P (P (A \cup B)) : \exists a \in A \exists b \in B z = (a, b)}$ , Relation, $dom R$ , $ran R$ , $fld R$ , and the specialisations "relation from $A$ to $B$ " and "relation on $A$ ").

[F3]

The empty function is the empty set, and $\emptyset$ is a function with empty domain and empty range; it is a bijection $\emptyset \to \emptyset = 0$ (A function is a relation $f$ with $(a, b) \in f$ and $(a, c) \in f$ implying $b = c$ ; $f : A \to B$ , the value $f (a)$ , domain and codomain, Relation, $dom R$ , $ran R$ , $fld R$ , and the specialisations "relation from $A$ to $B$ " and "relation on $A$ ").

[F4]

A bijection is in particular a surjection, and an at most countable nonempty set has a surjection from $N$ by the onto criterion; the criterion as stated assumes $A \neq \emptyset$ (Injection, surjection, bijection, A nonempty set is at most countable iff it is a surjective image of $N$ ).

Counterexample

technique · direct

1.1F1F3

$\emptyset \approx 0$ via the empty function, so $\emptyset$ is finite and hence at most countable.

1.2F2given

No function $f : N \to \emptyset$ exists. If $f$ were one, then $f \subseteq N \times \emptyset$ ; the product $N \times \emptyset$ is empty, so $f = \emptyset$ and $dom f = \emptyset$ , which is not $N$ since $0 \in N$ while $\emptyset$ has no elements. Equivalently, a value $f (0)$ would have to be an element of $\emptyset$ .

2.1step 1.1step 1.2F4∎

Hence $\emptyset$ is at most countable by step 1.1 but no function, and in particular no surjection, maps $N$ onto it by step 1.2, so the refuted claim fails and the nonemptiness hypothesis in the forward direction of A nonempty set is at most countable iff it is a surjective image of $N$ cannot be dropped.

Remarks

The failure is not about repetition of values, as in A nonempty surjective image of $N$ need not be equinumerous with $N$ , but about totality: a function out of $N$ must assign a value to $0$ , and there is no value to assign. This is exactly the empty case that the onto criterion A nonempty set is at most countable iff it is a surjective image of $N$ separates out.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

29 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

John K. Hunter, An Introduction to Real Analysis (complete author-hosted lecture notes, 307 pp.) (standard reference, not scraped)
Jiri Lebl, Basic Analysis I: Introduction to Real Analysis, Volume I (author-hosted complete book PDF) (standard reference, not scraped)

The empty set is at most countable but no function from NN is onto it