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.
Every natural-number-indexed list of nonempty sets has a choice function on its family of values
Statement
Let and let be a function with domain all of whose values are nonempty sets. Then the family of its values, , has a choice function (Choice function).
This is a theorem of ZF: its proof uses no form of the Axiom of Choice (The Axiom of Choice).
What is proved below is exactly the displayed statement, by induction on . The natural number serves as the index set in the von Neumann sense, (The natural numbers (von Neumann)), so " has domain " says precisely that the members of are listed as . The listing need not be injective, and is the set of values, so repetitions are harmless and are not counted.
The displayed statement and its proof use only a natural-number-indexed function. They do not identify an arbitrary finite family with a particular enumeration.
Facts & Assumptions
Given: A natural number , used as the index set , and a function with domain such that for every ; write for the family of values of .
denotes the statement: for every function with domain all of whose values are nonempty sets, the family has a choice function.
Induction principle: if holds and implies for every , then holds for every , where denotes the successor (The principle of mathematical induction, Addition of natural numbers).
A choice function for a family is a function with domain such that for every (Choice function).
and , so (The natural numbers (von Neumann)). Thus a function with domain restricts to a function with domain ; moreover, directly from the definition of image, iff for some or , so .
Proof
Base case: , so the only function with domain is the empty function, its family of values is , and the empty function has domain and satisfies the defining condition vacuously, so it is a choice function for ; hence holds.
Inductive hypothesis: fix and assume , that every function with domain whose values are all nonempty has a choice function for its family of values.
Let be an arbitrary function with domain all of whose values are nonempty sets; write and , the family of values of the restriction , so that .
The restriction is a function with domain , and every value of it is a value of , hence nonempty; so the inductive hypothesis applies to it and supplies a choice function for , a function with domain satisfying for every .
The set is one of the values of , hence nonempty, so there exists an element of ; fix one and call it .
Define ; its two pieces are functions with the disjoint domains and , so is a function, and its domain is .
Every is either or a member of ; in the first case , and in the second because is a choice function for . So throughout.
Hence is a choice function for , and since was an arbitrary function with domain with nonempty values, implies .
By the induction principle, holds for every : the family of values of any function whose domain is a natural number and whose values are nonempty has a choice function.
Remarks
- Later finiteness terminology. A finite set is defined later as one equinumerous with a natural number (Finite, countably infinite, countable, uncountable ↗). That terminology is not used in the proof above, which keeps its exact indexed-family scope.
- Where the Axiom of Choice would be needed, and why it is not needed here. Step 2.2 picks one element out of one nonempty set. That is a single existential instantiation, licensed by first-order logic alone. The induction performs one such instantiation per stage, and the stages are indexed by a natural number, so the process terminates. ZF cannot in general turn an arbitrary infinite family of nonempty sets into a simultaneous choice function; that is the gap The Axiom of Choice fills. An infinite family with a distinguished element in each member may still have an explicit choice function in ZF, as Russell's shoes and socks ↗ shows.
- Why the family is presented as an indexed one. Stated over "a family of exactly sets", the successor step would have to assert that deleting one member of a family of sets leaves exactly , which is a claim about cardinality and needs a theory of finiteness this page does not have. Indexed by , the same step is the restriction of a function, which is immediate from and costs nothing. Nothing else in the argument changes.
- The listing may repeat, and the argument is arranged so that repetition needs no separate treatment: is built by overwriting rather than by adjoining, so it is a function whether or not already occurs among . In particular may have strictly fewer than members.
- The lemma is not a special case of the Axiom of Choice that happens to be provable; it is the precise boundary of what is free. Russell's shoes and socks ↗ makes the boundary concrete, and Finite choice written out: a choice function for three sets ↗ works this induction out on a small family.
Depends on
Used by
- Tagged grid partitions and Riemann sums in ℝᵐ Definition
- The product set ∏_i ∈ I Xᵢ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space Definition
- A finite subset of any space is compact, so the compact separation clauses specialise to separating a point from a finite set in a Hausdorff space Example
- Finite choice written out: a choice function for three sets Example
- In any metric space the range of a convergent sequence together with its limit is compact, worked out for {0} ∪ {1/(k+1) : k ∈ ℕ} in ℝ Example
- Russell's shoes and socks Example
- With the discrete metric d(x,y) = 1 for x ≠ y, a space is compact iff it is totally bounded iff it is finite, and it is complete whatever its size Example
- A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it Lemma
- A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it Lemma
- A totally bounded metric space is bounded, every subspace of a totally bounded space is totally bounded, and the closure of a totally bounded subset is totally bounded Lemma
- Arbitrary products of completely regular spaces are completely regular Lemma
- Arbitrary products of regular spaces are regular Lemma
- Assuming countable choice, every countably compact paracompact Hausdorff space is compact Lemma
- Every open cover of a compact Hausdorff space has a finite open star-refinement Lemma
- For n ≥ 1 the product topology on n copies of the usual topology of ℝ is the metric topology of d_∞ on ℝⁿ, and hence also of d₁ and d₂, so ℝⁿ as a product and ℝⁿ as a metric space are one space Lemma
- The Samuel uniformity is totally bounded Lemma
- The quasicompact convention, why compactness of a subset is read intrinsically here, and what each result on this page costs in choice Remark
- What this page costs in choice: Riemann's criterion, the Darboux-Riemann equivalence and integrability of a monotone function are theorems of ZF; integrability of a continuous function inherits the single use of countable choice inside Heine-Cantor; and only the forward half of the Lebesgue criterion spends countable choice, once, at the countable union of null sets Remark
- Which results on this page spend dependent choice, which spend countable choice, and which are theorems of ZF Remark
- Why the criterion is about the product topology, and the choice cost of the compact separation lemmas Remark
- A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact Theorem
- A complete, totally bounded metric space is compact, proved from countable choice used exactly once Theorem
- A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism Theorem
- A map into a compact space whose graph is closed is continuous; so for a compact Hausdorff codomain, continuity and closedness of the graph are equivalent Theorem
- A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice Theorem
- A product of connected spaces is connected in the product topology, and that argument is a theorem of ZF; for an infinite index set it is the assertion that the product of nonempty spaces is nonempty that uses the Axiom of Choice Theorem
- A product of finitely many compact spaces is compact in the product topology Theorem
- A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions Theorem
- Alexander's subbase lemma: if every cover by members of a fixed subbasis has a finite subcover then the space is compact; the proof is an application of Zorn's lemma Theorem
- Dini's theorem on a closed interval: monotone pointwise convergence of continuous functions to a continuous limit is uniform Theorem
- In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones Theorem
- In any metric space compactness implies countable compactness and limit point compactness, and each of countable compactness and limit point compactness implies sequential compactness; every implication here is proved without a choice principle Theorem
- Products commute with subspaces; for infinite nonempty families, the closure identity overline∏ Aᵢ=∏ overlineAᵢ uses the Axiom of Choice Theorem
- ℚⁿ is a countable dense subset of ℝⁿ, and rational open boxes form a countable basis Theorem
- The Darboux and Riemann definitions agree: a bounded f on [a,b] is Darboux integrable with integral I if and only if for every real ε > 0 there is a real δ > 0 such that |S(f,P,ξ) - I| < ε for every tagged partition of mesh below δ Theorem
- The multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree Theorem
- Urysohn's lemma, under the axiom of dependent choice: in a normal space two disjoint closed sets are separated by a continuous function into [0,1], and conversely such a space is normal Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 33 results over 14 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
- Axiom of choice (Wikipedia) (standard reference, not scraped)
- Choice function (Wikipedia) (standard reference, not scraped)