Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableverified 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.

Choice function

Definition

Let F be a family of sets, every member of which is nonempty. A choice function for F is a function (A function is a relation f with (a,b)∈f and (a,c)∈f implying b=c; f:A→B, the value f(a), domain and codomain) g:F→⋃Fsuch thatg(S)∈S  for every S∈F.

Given a set X, a choice function on X means a choice function for the family P(X)∖{∅} (The power set P(x)={ z:z⊆x }, The difference a∖b, the symmetric difference a△b, and the complement X∖a relative to a set X) of nonempty subsets of X.

Remarks

  • The requirement is only that g pick some element of each member. Nothing requires the choices to be coherent, definable, or computable, and this is exactly where the difficulty lies: for a single nonempty set S the existence of an element to pick is immediate, and for a family presented as the values of a function on a natural number the picks can be made one after another (Every natural-number-indexed list of nonempty sets has a choice function on its family of values ↗). What is not available in ZF is a simultaneous choice across an arbitrary family.
  • A choice function often exists for a concrete family with no appeal to any axiom, because the family carries extra structure that names a canonical element. Every nonempty set of natural numbers has a least element, so S↦min⁡S is an explicit choice function on N (min⁡ is a choice function on N ↗). The contrast with families that admit no such rule is the content of Russell's shoes and socks ↗.
  • Members of F must be nonempty: no function can select an element of ∅. The family F itself is allowed to be empty, and the empty function is then a choice function for it.

Depends on

Used by

Dependency tree · two levels

17 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