Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)verified 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 iIXi\prod_{i \in I} X_i 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 II be a set and let XiX_i be a set for each iIi \in I. The product is

iIXi  :=  {x:x is a function with domain I and x(i)Xi for every iI},\prod_{i \in I} X_i \;:=\; \Big\{\, x : x \text{ is a function with domain } I \text{ and } x(i) \in X_i \text{ for every } i \in I \,\Big\},

and we write xi:=x(i)x_i := x(i), the ii-th coordinate of xx. 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 jIj \in I the jj-th projection is

πj:iIXiXj,πj(x):=xj.\pi_j : \prod_{i \in I} X_i \to X_j, \qquad \pi_j(x) := x_j .

Notation for a finite product. For I=nI = n a natural number, which is the set {0,1,,n1}\{0, 1, \dots, n-1\} of its predecessors, an element of k<nXk\prod_{k<n} X_k is a function on nn and we write it (x0,,xn1)(x_0, \dots, x_{n-1}). In particular I=2I = 2 gives the binary product, written X×YX \times Y for i<2Xi\prod_{i<2} X_i with X0=XX_0 = X and X1=YX_1 = Y, whose elements are written (u,v)(u,v) for the function 0u0 \mapsto u, 1v1 \mapsto v. This is the only meaning the symbol X×YX \times 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 Xi0X_{i_0} is empty then the product is empty, since no function can take a value in Xi0X_{i_0}. Conversely, suppose every XiX_i is nonempty.

  • For I=nI = 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 iXii \mapsto X_i on nn supplies a choice function gg for the family of values, and x(i):=g(Xi)x(i) := g(X_i) defines a member of k<nXk\prod_{k<n} X_k.
  • For an arbitrary II the assertion "iIXi\prod_{i \in I} X_i \ne \varnothing whenever every XiX_i 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 XiX_i carry a topology Ti\mathcal{T}_i (Topology on a set, open and closed sets, clopen sets, the closed-set axiomatisation, and the coarser/finer comparison). Put

R  :=  {iIUi  :  UiTi for every iI},\mathcal{R} \;:=\; \Big\{\, \prod_{i \in I} U_i \;:\; U_i \in \mathcal{T}_i \text{ for every } i \in I \,\Big\},

the family of boxes. R\mathcal{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\prod_i X_i, so it covers the product, and it is closed under binary intersections, since

(iUi)(iVi)=i(UiVi)\Big(\prod_i U_i\Big) \cap \Big(\prod_i V_i\Big) = \prod_i (U_i \cap V_i)

and each UiViU_i \cap V_i is open by (T3). The topology it generates is the box topology T\mathcal{T}^{\square}, and R\mathcal{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Π\mathcal{T}^{\Pi} on iXi\prod_i X_i is the initial topology of the family of projections (πi)iI(\pi_i)_{i \in 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  :=  {πi1[U]:iI, UTi},πi1[U]=jIWj  with Wi=U and Wj=Xj for ji.\mathcal{G} \;:=\; \{\, \pi_i^{-1}[U] : i \in I,\ U \in \mathcal{T}_i \,\}, \qquad \pi_i^{-1}[U] = \prod_{j \in I} W_j \ \text{ with } W_i = U \text{ and } W_j = X_j \text{ for } j \ne 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\mathcal{G} form a basis for TΠ\mathcal{T}^{\Pi}, and those finite intersections are exactly the boxes with all but finitely many factors unrestricted:

RΠ  =  {iIUi  :  UiTi for every i, and Ui=Xi for all but finitely many i}.\mathcal{R}^{\Pi} \;=\; \Big\{\, \prod_{i \in I} U_i \;:\; U_i \in \mathcal{T}_i \text{ for every } i, \text{ and } U_i = X_i \text{ for all but finitely many } i \,\Big\}.

Indeed the intersection of πi11[U1],,πin1[Un]\pi_{i_1}^{-1}[U_1], \dots, \pi_{i_n}^{-1}[U_n] is the box whose factor at ii is the intersection of those UmU_m with im=ii_m = i and is XiX_i when no imi_m equals ii; and the intersection of no members is the whole product, the box with every factor XiX_i. Conversely a box with Ui=XiU_i = X_i off a finite set is such an intersection. Members of RΠ\mathcal{R}^{\Pi} are called basic product-open sets, and members of R\mathcal{R} boxes. So RΠR\mathcal{R}^{\Pi} \subseteq \mathcal{R}, with equality when II is a natural number.

The empty product. For I=I = \varnothing there is exactly one function with domain \varnothing, the empty function, so iXi\prod_{i \in \varnothing} X_i is a one-point set. A one-point set carries exactly one topology, namely {,{}}\{\varnothing, \{\varnothing\}\}, 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\prod_i X_i 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\mathcal{R}^{\Pi} \subseteq \mathcal{R}. They agree whenever II is finite; and, assuming the Axiom of Choice, for a family of nonempty spaces they differ for infinite II 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)iIx = (x_i)_{i \in I} is notation for the function xx. The finite case recovers the familiar tuple, and the identification of k<nR\prod_{k<n}\mathbb{R} with the Rn\mathbb{R}^n of Rn\mathbb{R}^n as the set of functions nRn \to \mathbb{R}, and d1d_1, d2d_2, dd_\infty are metrics on it is literal, that item defining Rn\mathbb{R}^n as the set of functions nRn \to \mathbb{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 40 more results.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 62 results over 25 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