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 cardinality of a finite set
Definition
Throughout this page is the set of von Neumann naturals (The natural numbers (von Neumann)): , , and is itself the set of its predecessors, the order being the additive order of Order on the natural numbers identified with membership in On the order is membership: . Write when a bijection exists (Equinumerous sets, and , Injection, surjection, bijection). A set is finite when for some (Finite, countably infinite, countable, uncountable).
Definition. Let be a finite set. Then there is exactly one with , and we write
the cardinality, or number of elements, of . The notation is defined for finite only, and its value is a natural number.
Why exactly one, which is the whole content of the definition. At least one such exists: that is literally what " is finite" says. At most one exists: if and with , then , because the inverse of a bijection is a bijection, and hence , because a composition of bijections is a bijection (Injection, surjection, bijection); and forces by claim 3 of The pigeonhole principle on . So names a single natural number and not a family of choices.
Four consequences, proved here because everything on this page uses them.
(a) for every . The identity map is a bijection , so ; thus is finite and the unique natural equinumerous with it is itself.
(b) , and a finite satisfies if and only if . Since , part (a) gives . Conversely, if then there is a bijection ; were some , the value would be an element of , and has none, so .
(c) Transport along a bijection. If is finite and is a bijection, then is finite and . Indeed through and , so by transitivity.
(d) Equality of cardinalities is equinumerosity. For finite and : if and only if . If the cardinalities agree then ; conversely gives by (c).
Definition references
Remarks
-
contains here, and that is not a detail. Every index range on this page starts at , a one-element set has cardinality , and is never a positive-integer-only object. A statement about that is true only for must say so.
-
is a natural number, not a cardinal number. The theory of cardinals (Cardinal (initial ordinal) and cardinality ↗) is developed much later in the library and nothing here uses it, or any cardinal arithmetic: the pointer is orientation only. What makes the notation legitimate at this point in the reading order is exactly claim 3 of The pigeonhole principle on , and nothing more.
-
What the definition does not supply. It asserts that some bijection exists; it does not single one out, and nothing in the library does. Two sets can have equal cardinality with no distinguished bijection between them, which is the point of the counterexample on this page's companion.