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

The product set ∏i∈IXi 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

The product set. Let I be a set and let Xi be a set for each i∈I. The product is

∏i∈IXi  :=  { x:x is a function with domain I and x(i)∈Xi for every i∈I },

and we write xi:=x(i), the i-th coordinate of x. Two elements of the product are equal exactly when they agree at every index, functions being equal when they have the same domain and the same values. For j∈I the j-th projection is

πj:∏i∈IXi→Xj,πj(x):=xj.

Notation for a finite product. For I=n a natural number, which is the set {0,1,…,n−1} of its predecessors, an element of ∏k<nXk is a function on n and we write it (x0,…,xn−1). In particular I=2 gives the binary product, written X×Y for ∏i<2Xi with X0=X and X1=Y, whose elements are written (u,v) for the function 0↦u, 1↦v. This is the only meaning the symbol X×Y carries on this page.

Two facts about when the product is nonempty, stated because they are used and because they cost something. If some Xi0 is empty then the product is empty, since no function can take a value in Xi0. Conversely, suppose every Xi is nonempty.

  • For I=n a natural number, the product is nonempty, and this is a theorem of ZF: Every natural-number-indexed list of nonempty sets has a choice function on its family of values applied to the function i↦Xi on n supplies a choice function g for the family of values, and x(i):=g(Xi) defines a member of ∏k<nXk.
  • For an arbitrary I the assertion "∏i∈IXi≠∅ whenever every Xi is nonempty" is the Axiom of Choice: it is the formulation recorded in The Axiom of Choice, and the choice function of Choice function is exactly a point of the product of a family by itself. Every use of it below is flagged at the step that spends it.

The box topology. Now let each Xi carry a topology Ti (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). Put

R  :=  { ∏i∈IUi  :  Ui∈Ti for every i∈I },

the family of boxes. R is a basis for a topology (A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis): it contains ∏iXi, so it covers the product, and it is closed under binary intersections, since

(∏iUi)∩(∏iVi)=∏i(Ui∩Vi)

and each Ui∩Vi is open by (T3). The topology it generates is the box topology T□, and R is a basis for it (Basis and subbasis for a topology, and the topology generated by a family of sets).

The product topology. The product topology TΠ on ∏iXi is the initial topology of the family of projections (πi)i∈I (The initial topology of a family of maps into spaces and the final topology of a family of maps out of spaces, and the subspace topology as the model initial topology): the topology generated by the subbasis

G  :=  { πi−1[U]:i∈I, U∈Ti },πi−1[U]=∏j∈IWj  with Wi=U and Wj=Xj for j≠i.

By A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis the finite intersections of members of G form a basis for TΠ, and those finite intersections are exactly the boxes with all but finitely many factors unrestricted:

RΠ  =  { ∏i∈IUi  :  Ui∈Ti for every i, and Ui=Xi for all but finitely many i }.

Indeed the intersection of πi1−1[U1],…,πin−1[Un] is the box whose factor at i is the intersection of those Um with im=i and is Xi when no im equals i; and the intersection of no members is the whole product, the box with every factor Xi. Conversely a box with Ui=Xi off a finite set is such an intersection. Members of RΠ are called basic product-open sets, and members of R boxes. So RΠ⊆R, with equality when I is a natural number.

The empty product. For I=∅ there is exactly one function with domain ∅, the empty function, so ∏i∈∅Xi is a one-point set. A one-point set carries exactly one topology, namely {∅,{∅}}, since a topology must contain the empty set and the whole set and there is nothing else to contain (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison); so the box topology and the product topology agree there, and both equal the discrete topology and the indiscrete topology (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies), which coincide on a one-point set. There are no projections to speak of, and the initial topology of the empty family is indeed the indiscrete one (The initial topology of a family of maps into spaces and the final topology of a family of maps out of spaces, and the subspace topology as the model initial topology).

Convention. Unless the box topology is named explicitly, ∏iXi always carries the product topology in this library. That is not a matter of taste: the product topology is the one with the characteristic property of the next item, and the box topology has no such property.

Remarks

  • Where the two topologies actually differ. The box topology is finer than the product topology by construction, since RΠ⊆R. They agree whenever I is finite; and, assuming the Axiom of Choice, for a family of nonempty spaces they differ for infinite I as soon as infinitely many factors have a nonempty proper open subset. Nonemptiness is not decoration: if one factor is empty then the product is empty and carries exactly one topology, so the two agree however the other factors are chosen. Both statements are proved two items below, with that hypothesis, and the failure is recorded on this page as a false statement.

  • The product set is a set of functions, and that is not a technicality. The factors are indexed by an arbitrary set, so there is no "list" to write down; writing x=(xi)i∈I is notation for the function x. The finite case recovers the familiar tuple, and the identification of ∏k<nR with the Rn of Rn as the set of functions n→R, and d1, d2, d∞ are metrics on it is literal, that item defining Rn as the set of functions n→R.

  • The projections carry no hypothesis. They are defined for every product, including the empty one and products with an empty factor; what does need a hypothesis is their surjectivity, which is the point at which choice enters and which is stated separately in the next item.

Depends on

Used by

…and 94 more results.

Dependency tree · two levels

26 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