Alphabeta Math
DefinitionDefinition: AI-adaptedProof: AI-generatedjudge pass (z-ai/glm-5.2)audited 2026-07-29
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 ∣A∣ of a finite set

Definition

Throughout this page N is the set of von Neumann naturals (The natural numbers N (von Neumann)): 0=∅, σ(n)=n∪{n}, and n={ m∈N:m<n } is itself the set of its predecessors, the order being the additive order of Order on the natural numbers identified with membership in On N the order is membership: m<n  ⟺  m∈n. Write A≈B when a bijection A→B exists (Equinumerous sets, A≈B and A⪯B, Injection, surjection, bijection). A set A is finite when A≈n for some n∈N (Finite, countably infinite, countable, uncountable).

Definition. Let A be a finite set. Then there is exactly one n∈N with A≈n, and we write

∣A∣:=that n,

the cardinality, or number of elements, of A. The notation ∣A∣ is defined for finite A only, and its value is a natural number.

Why exactly one, which is the whole content of the definition. At least one such n exists: that is literally what "A is finite" says. At most one exists: if A≈n and A≈m with n,m∈N, then n≈A, because the inverse of a bijection is a bijection, and hence n≈m, because a composition of bijections is a bijection (Injection, surjection, bijection); and n≈m forces n=m by claim 3 of The pigeonhole principle on N. So ∣A∣ names a single natural number and not a family of choices.

Four consequences, proved here because everything on this page uses them.

(a) ∣n∣=n for every n∈N. The identity map idn is a bijection n→n, so n≈n; thus n is finite and the unique natural equinumerous with it is n itself.

(b) ∣∅∣=0, and a finite A satisfies ∣A∣=0 if and only if A=∅. Since 0=∅, part (a) gives ∣∅∣=0. Conversely, if ∣A∣=0 then there is a bijection f:A→∅; were some a∈A, the value f(a) would be an element of ∅, and ∅ has none, so A=∅.

(c) Transport along a bijection. If A is finite and f:A→B is a bijection, then B is finite and ∣B∣=∣A∣. Indeed B≈A through f−1 and A≈∣A∣, so B≈∣A∣ by transitivity.

(d) Equality of cardinalities is equinumerosity. For finite A and B: ∣A∣=∣B∣ if and only if A≈B. If the cardinalities agree then A≈∣A∣=∣B∣≈B; conversely A≈B gives ∣B∣=∣A∣ by (c).

Remarks

  • N contains 0 here, and that is not a detail. Every index range on this page starts at 0, a one-element set has cardinality 1={0}, and ∣A∣ is never a positive-integer-only object. A statement about ∣A∣ that is true only for ∣A∣≥1 must say so.

  • ∣A∣ 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 N, and nothing more.

  • What the definition does not supply. It asserts that some bijection A→∣A∣ 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.

Depends on

Used by

…and 217 more results.

Dependency tree · two levels

23 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