Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)verified 2026-07-26 (claude-opus-5)
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.

Finite, countably infinite, countable, uncountable

Definition

Recall that a natural number is a von Neumann natural (The natural numbers N (von Neumann)): 0=∅ and σ(n)=n∪{n}, so that

n={ m∈N:m<n }={0,1,…,n−1}

is itself the set of its predecessors. Here < is the order of Order on the natural numbers, which is defined additively, so the displayed identity is a theorem and not a convention: it is On N the order is membership: m<n  ⟺  m∈n, proved immediately above. Let A be a set, and let ≈ be equinumerosity (Equinumerous sets, A≈B and A⪯B).

  • A is finite if A≈n for some n∈N.
  • A is countably infinite if A≈N.
  • A is at most countable if it is finite or countably infinite.
  • A is uncountable if it is not at most countable.

Remarks

  • Convention: in this library "countable" alone always means "at most countable", so a finite set is countable. This is the convention of Halmos and of Tao, and it is the one that makes the theorems on this page read cleanly: subsets, products and unions of countable sets are countable, with no finite/infinite case split in the statement. The competing convention, used by Rudin among others, reserves "countable" for "countably infinite" and says "at most countable" for the disjunction. Under that convention every statement below still holds after replacing "countable" with "at most countable", but several would become false as literally written. Where the distinction matters, the long forms "countably infinite" and "at most countable" are used in full, and "uncountable" always means "not at most countable", on which the two conventions agree.

  • The three classes are exhaustive by construction: every set is finite, countably infinite, or uncountable, since "uncountable" is defined as the negation of the disjunction. That they are also mutually exclusive, that is, that no set is both finite and countably infinite, is a genuine theorem amounting to N≉n for every n∈N, and it is proved immediately above as claim 4 of The pigeonhole principle on N. So a countably infinite set is never finite, and "A is infinite", meaning not finite, is implied by A≈N. The same lemma pins down finiteness itself: by its claim 3 a finite set is equinumerous with exactly one natural number, so the number of elements of a finite set is well defined, and by its claim 5 no finite set is equinumerous with a proper subset of itself.

  • What the exclusivity is and is not used for below. Nothing on this page needs it in order to run: the infinitude of Q, for instance, is obtained by exhibiting a bijection Q≈N directly (Q is countably infinite) rather than by ruling out finiteness. It is used when the continuum hypothesis is instantiated at N (The continuum hypothesis, and what this page does not prove), where N must be infinite as a fact rather than as a convention.

  • 0 and the empty set. 0=∅, and A≈0 holds exactly when A=∅, so the empty set is finite. This matters in the proofs below, where the empty case is always separated out: a surjection N→A cannot exist when A=∅, which is why A nonempty set is at most countable iff it is a surjective image of N assumes A nonempty.

  • Countability is a property of a set alone, not of a set with structure. In particular Q is countable while carrying a dense order, and R is uncountable; neither statement says anything on its own about the order or the arithmetic those sets carry.

Depends on

Used by

…and 198 more results.

Dependency tree · two levels

20 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