CounterexampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

Two sets of the same finite cardinality between which the bijection is not unique

Statement refuted

Refuted claim: two equinumerous finite sets admit exactly one bijection between them.

The witness is $A := 2 = \{\varnothing,\{\varnothing\}\} = \{0,1\}$ and $B := [2]^{1} = \{\{0\},\{1\}\}$ , the set of one-element subsets of $2$ . Both have cardinality $2$ , and there are exactly two bijections between them.

Facts & Assumptions

Given: $A = 2 = \{0,1\}$ with $0 = \varnothing$ and $1 = \{0\}$ (The natural numbers $\mathbb{N}$ (von Neumann)), and $B = [2]^{1}$ , the set of $1$ -element subsets of $2$ .

[L1]

$\lvert n\rvert = n$ for a natural $n$ , and $\lvert A\rvert$ is the unique natural equinumerous with $A$ (The cardinality $\lvert A\rvert$ of a finite set).

[L2]

$\lvert [X]^{k}\rvert = \binom{\lvert X\rvert}{k}$ and $\binom{n}{1} = n$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$ ).

[L3]

The set of bijections between two finite sets of common cardinality $n$ has exactly $n!$ elements (A finite set $A$ with $\lvert A\rvert = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality), and $2! = 2$ (The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $\mathbb{N}$ ).

[L4]

A bijection is an injective surjection (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A \preceq B$ ).

[L5]

Claim 3 of The pigeonhole principle on $\mathbb{N}$ : a finite set is equinumerous with exactly one natural number.

Counterexample

technique · direct

1.1

The two sets and their cardinalities. $A = 2$ has $\lvert A\rvert = 2$ by [L1]. The elements of $B = [2]^{1}$ are the one-element subsets of $\{0,1\}$ , namely $\{0\}$ and $\{1\}$ , so $\lvert B\rvert = \binom{2}{1} = 2$ by [L2]. Hence $\lvert A\rvert = \lvert B\rvert$ .

givenL1L2

2.1

Two distinct bijections. Let $f : A \to B$ be $f(0) = \{0\}$ , $f(1) = \{1\}$ , and let $g : A \to B$ be $g(0) = \{1\}$ , $g(1) = \{0\}$ . Each is injective, its two values being distinct, and each is surjective, its image being all of $B$ ; so both are bijections by [L4]. They are distinct, since $f(0) = \{0\} \ne \{1\} = g(0)$ .

step 1.1L4construct

3.1

There are exactly two. By [L3] the set of bijections $A \to B$ has $2! = 2$ elements, so $f$ and $g$ of step 2.1 are all of them.

step 1.1L3

4.1

The refuted claim fails: $\lvert A\rvert = \lvert B\rvert$ holds, and there are two bijections $A \to B$ , not one. The cardinality $\lvert A\rvert$ of a finite set asserts only that some bijection $A \to \lvert A\rvert$ exists; [L5] makes the resulting natural number unique, not the witnessing map.

step 2.1step 3.1L1L5∎

Remarks

What is unique and what is not. Cardinality is a well-defined function of the set, but a bijection witnessing an equality of cardinalities need not be unique. Whenever a construction is made "along a bijection", one has to check, as The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form does, that the result does not depend on which bijection was used.
The count grows fast. For $\lvert A\rvert = n$ there are $n!$ bijections onto any set of the same cardinality (A finite set $A$ with $\lvert A\rvert = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality), so the bijection is unique only for $n \le 1$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 70 results over 25 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Cardinality (Wikipedia) (standard reference, not scraped)
Bijective proof (Wikipedia) (standard reference, not scraped)
P. Halmos, Naive Set Theory, §13 (standard reference, not scraped)