TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge 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.

König's theorem: assuming the Axiom of Choice, if $κ_{i} < λ_{i}$ for every $i \in I$ then $\sum_{i \in I} κ_{i} < \prod_{i \in I} λ_{i}$

Statement

Assume the Axiom of Choice (The Axiom of Choice). Let $I$ be a set and let $(κ_{i})_{i \in I}$ and $(λ_{i})_{i \in I}$ be families of cardinals (Cardinal (initial ordinal) and cardinality) with

$κ_{i} < λ_{i} for every i \in I .$

Then

$\sum_{i \in I} κ_{i} < \prod_{i \in I} λ_{i}$

(The sum $\sum_{i \in I} κ_{i}$ and the product $\prod_{i \in I} κ_{i}$ of an indexed family of cardinals, defined under the Axiom of Choice).

The hypothesis is named in the statement, not only in the facts, and it is spent twice: once in the definition of the two sides, which are cardinalities of sets ZF does not well-order, and once in the diagonal step of the proof, which selects an omitted value in each coordinate at the same time.

Facts & Assumptions

Given: The Axiom of Choice; a set $I$ ; families of cardinals $(κ_{i})_{i \in I}$ , $(λ_{i})_{i \in I}$ with $κ_{i} < λ_{i}$ for every $i$ . Write $S = ⋃_{i \in I} ({i} \times κ_{i})$ and $P$ for the set of functions $f$ on $I$ with $f (i) \in λ_{i}$ for every $i$ .

[L1]

$\sum_{i \in I} κ_{i} = ∣ S ∣$ and $\prod_{i \in I} λ_{i} = ∣ P ∣$ , both defined because the Axiom of Choice well-orders every set (The sum $\sum_{i \in I} κ_{i}$ and the product $\prod_{i \in I} κ_{i}$ of an indexed family of cardinals, defined under the Axiom of Choice, The well-ordering theorem, Cardinal sum $κ \oplus λ$ , product $κ \otimes λ$ and exponentiation $κ^{λ}$ , and why they are written apart from the ordinal operations).

[L2]

For cardinals $κ \leq λ$ iff $κ ⪯ λ$ , and $A ⪯ B$ with both well-orderable gives $∣ A ∣ \leq ∣ B ∣$ (claim (a) of Commutativity, associativity, distributivity and monotonicity of $\oplus$ and $\otimes$ , the unit laws, the two exponent laws, and $κ \leq λ$ if and only if $κ$ injects into $λ$ ).

[L3]

$X \approx ∣ X ∣$ for well-orderable $X$ , and equinumerous sets receive the same cardinality (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, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ).

[L4]

Ordinals satisfy trichotomy, $α \subseteq β$ iff $α \in β$ or $α = β$ , $α \notin α$ , and every nonempty set of ordinals has an $\in$ -least element (Trichotomy and well-ordering of the ordinals, Basic closure properties of ordinals, Well-order and well-ordered set).

[L5]

A product of nonempty sets is nonempty: if $X_{i} \neq \emptyset$ for every $i \in I$ then some function $g$ on $I$ has $g (i) \in X_{i}$ for all $i$ (The Axiom of Choice, Choice function).

[L6]

A composition of injections is an injection, and a bijection is in particular a surjection (Injection, surjection, bijection).

Proof

technique · contradiction

1.1

The map $h$ sending $(i, ξ) \in S$ to the function on $I$ taking the value $ξ$ at $i$ and the value $κ_{j}$ at each $j \neq i$ takes values in $P$ , because $ξ \in κ_{i} \subseteq λ_{i}$ and $κ_{j} \in λ_{j}$ by [L4]; and it is injective, since $h (i, ξ) = h (i^{'}, ξ^{'})$ with $i \neq i^{'}$ would give $ξ = κ_{i}$ at the coordinate $i$ , impossible as $ξ \in κ_{i}$ and $κ_{i} \notin κ_{i}$ , so $i = i^{'}$ and then $ξ = ξ^{'}$ .

L4L6

2.1

Hence $S ⪯ P$ and $\sum_{i \in I} κ_{i} \leq \prod_{i \in I} λ_{i}$ by [L1] and [L2].

step 1.1L1L2

3.1

Suppose, for contradiction, that $\sum_{i \in I} κ_{i} < \prod_{i \in I} λ_{i}$ fails; then trichotomy and step 2.1 force $\sum_{i \in I} κ_{i} = \prod_{i \in I} λ_{i}$ .

step 2.1L4assume-contra

4.1

Then $S \approx ∣ S ∣ = ∣ P ∣ \approx P$ by [L1] and [L3], so there is a bijection $F : S \to P$ , in particular a surjection.

step 3.1L1L3L6

5.1

For each $i \in I$ put $B_{i} = {F (i, ξ) (i) : ξ \in κ_{i}} \subseteq λ_{i}$ ; the map sending $b \in B_{i}$ to the $\in$ -least $ξ \in κ_{i}$ with $F (i, ξ) (i) = b$ is an injection $B_{i} \to κ_{i}$ by [L4], so $∣ B_{i} ∣ \leq κ_{i} < λ_{i}$ by [L2], and therefore $B_{i} \neq λ_{i}$ and $λ_{i} ∖ B_{i} \neq \emptyset$ .

step 4.1L2L3L4

6.1

By [L5] there is a function $g$ on $I$ with $g (i) \in λ_{i} ∖ B_{i}$ for every $i$ , and $g \in P$ since $λ_{i} ∖ B_{i} \subseteq λ_{i}$ .

step 5.1L5

7.1

But $g \neq F (i, ξ)$ for every $(i, ξ) \in S$ , because the two differ at the coordinate $i$ , where $F (i, ξ) (i) \in B_{i}$ and $g (i) \notin B_{i}$ ; so $g$ is outside the image of $F$ and $F$ is not surjective, contradicting step 4.1. Therefore the assumption of step 3.1 is false and $\sum_{i \in I} κ_{i} < \prod_{i \in I} λ_{i}$ .

step 4.1step 5.1step 6.1discharge-contradiction∎

Remarks

The set form of the theorem implies the Axiom of Choice outright, in one line. Suppose it were true that for families of sets with $A_{i} ≺ B_{i}$ for every $i$ one had $⨆_{i} A_{i} ≺ \prod_{i} B_{i}$ . Given nonempty sets $B_{i}$ , take $A_{i} = \emptyset$ : then $A_{i} ⪯ B_{i}$ and $A_{i} \approx̸ B_{i}$ , so $A_{i} ≺ B_{i}$ ; the conclusion gives $\emptyset ≺ \prod_{i} B_{i}$ , hence $\prod_{i} B_{i} \approx̸ \emptyset$ and $\prod_{i} B_{i} \neq \emptyset$ , which is exactly the product formulation of The Axiom of Choice. So the hypothesis of this theorem is not an artefact of the proof, and the version stated above, for cardinals, is the one that can be written down at all without presupposing choice somewhere.

Where the diagonal is. Step 5.1 says that the $i$ -th block of $S$ , which has only $κ_{i}$ members, cannot exhaust the $λ_{i}$ possible values in the $i$ -th coordinate. Step 6.1 assembles the omitted values into a single element of the product. This is Cantor's diagonal argument with an arbitrary index set in place of $N$ , and with the two-element set replaced by $λ_{i}$ ; the one thing it needs beyond Cantor's version is the simultaneous selection, which is where the Axiom of Choice is spent the second time.

What it is used for on this page. With $λ_{i}$ constant the product becomes an exponential, and the resulting inequality bounds the cofinality of a power from below; that consequence is Assuming the Axiom of Choice: $κ < κ^{cf (κ)}$ for every infinite cardinal $κ$ , and $cf (2^{κ}) > κ$ ; in particular $cf (2^{ℵ_{0}}) > ℵ_{0}$ , and it is the only ZFC constraint on $2^{ℵ_{0}}$ established here.

Depends on

Used by

Dependency tree · two levels

41 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

K. Kearnes, Cardinal Arithmetic, König’s Lemma (standard reference, not scraped)
König's theorem (set theory) (Wikipedia) (standard reference, not scraped)
T. Jech, Set Theory, 3rd millennium ed., Ch. 5 (Cardinal arithmetic) (standard reference, not scraped)

König's theorem: assuming the Axiom of Choice, if κi<λiκi​<λi​ for every i∈Ii∈I then ∑i∈Iκi<∏i∈Iλi∑i∈I​κi​<∏i∈I​λi​