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

The sum ∑i∈Iκi and the product ∏i∈Iκi of an indexed family of cardinals, defined under the Axiom of Choice

Definition

Assume the Axiom of Choice (The Axiom of Choice). Let I be a set and (κi)i∈I a family of cardinals (Cardinal (initial ordinal) and cardinality), that is, a function on I whose value at i is the cardinal κi. Put

⨆i∈Iκi  :=  ⋃i∈I({i}×κi),∏i∈Isetκi  :=  { f:f is a function on I with f(i)∈κi for all i∈I },

both sets by Replacement, Union and Power Set. The sum and product of the family are their cardinalities:

∑i∈Iκi  :=  ∣⨆i∈Iκi∣,∏i∈Iκi  :=  ∣∏i∈Isetκi∣.

Why the hypothesis is in the definition. Both right-hand sides are cardinalities of sets that ZF does not well-order. Under the Axiom of Choice every set is well-orderable (The well-ordering theorem) and both values exist (A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used). Nothing else is being assumed: the two sets themselves are constructed in ZF, and the family (κi)i∈I is a function, so no representative is selected.

The finite cases are the operations already defined. Take I=2={0,1}. Then ⨆i∈2κi=({0}×κ0)∪({1}×κ1)=κ0⊔κ1 literally, so ∑i∈2κi=κ0⊕κ1 (Cardinal sum κ⊕λ, product κ⊗λ and exponentiation κλ, and why they are written apart from the ordinal operations); and f↦(f(0),f(1)) is a bijection from ∏i∈2setκi onto κ0×κ1, with inverse (a,b)↦{(0,a),(1,b)}, so ∏i∈2κi=κ0⊗κ1 by A set equinumerous with some ordinal has a least such ordinal, that ordinal is a cardinal, and equinumerous sets get the same one; no choice principle is used.

A constant family recovers ⊗ and exponentiation. If κi=κ for every i∈I and λ=∣I∣, then ⨆i∈Iκ=I×κ and ∏i∈Isetκ=Iκ, so

∑i∈Iκ=λ⊗κ,∏i∈Iκ=κλ,

by the transport clause of Cardinal sum κ⊕λ, product κ⊗λ and exponentiation κλ, and why they are written apart from the ordinal operations together with Disjoint union, cartesian product, function space and power set respect equinumerosity, and for ordinals α,β the sets α⊔β and α×β carry explicit well-orders, so their cardinalities exist in ZF and Injection, surjection, bijection.

Remarks

The product set is the set of choice functions. An element of ∏i∈Isetκi picks one element of κi for every i, which is exactly a choice function for the family (Choice function). So the assertion "the product set is nonempty when every κi is nonempty" is the Axiom of Choice for that family, in the formulation recorded in The Axiom of Choice, and it is not an incidental consequence of the definition.

Why the sum tags its blocks. Without the tag {i}×κi the union ⋃iκi would be a union of ordinals, which is the supremum of the family and not its sum: with κi=1 for every i∈ω the untagged union is 1, while the sum is ℵ0, and the difference is exactly that the tagged blocks are disjoint. The tagging is the same device Cardinal sum κ⊕λ, product κ⊗λ and exponentiation κλ, and why they are written apart from the ordinal operations uses for ⊕, applied to an arbitrary index set.

What is not defined here. Nothing is said about ∑ and ∏ over an index set for which the family has no cardinal values, and nothing is said in ZF alone. The theorem this definition exists for, König's theorem: assuming the Axiom of Choice, if κi<λi for every i∈I then ∑i∈Iκi<∏i∈Iλi, carries the same hypothesis for the same reason.

Depends on

Used by

Dependency tree · two levels

34 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