TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

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 rule: $\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert$ , and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$

Statement

If $A$ and $B$ are finite then $A \times B$ is finite and $\lvert A \times B\rvert = \lvert A\rvert \cdot \lvert B\rvert$ (The cardinality $\lvert A\rvert$ of a finite set).
Let $m \in \mathbb{N}$ and let $A_0, \dots, A_{m-1}$ be finite sets. Write $\prod_{i<m} A_i := \{\, f : f \text{ is a function with domain } m \text{ and } f(i) \in A_i \text{ for every } i < m \,\}.$ Then $\prod_{i<m} A_i$ is finite and $\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert$ , the right-hand product being the $\mathbb{N}$ -valued one of Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$ .

At $m = 0$ clause 2 reads $\big\lvert\prod_{i<0} A_i\big\rvert = 1$ : there is exactly one function with domain $\varnothing$ , the empty function, and the empty product is $1$ . Both sides are computed, not stipulated.

Facts & Assumptions

Given: Finite sets $A$ , $B$ and a finite list $A_0, \dots, A_{m-1}$ of finite sets. Recall $\sigma(m) = m \cup \{m\}$ and $m = \{\,i : i < m\,\}$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

Cardinality (The cardinality $\lvert A\rvert$ of a finite set): $\lvert A\rvert$ is the unique natural with $A \approx \lvert A\rvert$ ; $\lvert n\rvert = n$ ; and a bijection transports finiteness and cardinality.

[L3]

The sum rule (The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition): a family of pairwise disjoint finite sets indexed by a finite set has finite union, whose cardinality is the sum over that index set of the cardinalities.

[L4]

Sums over a finite index set (The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form): $\sum_{i \in S} c = \lvert S\rvert \cdot c$ for a constant $c$ .

[L5]

Recursion clause for the $\mathbb{N}$ -valued product (Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$ ): $\prod_{i<0} c_i = 1$ and $\prod_{i<\sigma(m)} c_i = \big(\prod_{i<m} c_i\big)\cdot c_m$ .

[L6]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A \preceq B$ ): a map with a two-sided inverse is a bijection, and composites of bijections are bijections.

[L7]

Arithmetic: multiplication of naturals is commutative (Multiplication is commutative, Multiplication of natural numbers); and $m = \{\,i : i<m\,\}$ , $\sigma(m) = m \cup \{m\}$ , $m \notin m$ (On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ , The natural numbers $\mathbb{N}$ (von Neumann)).

Proof

technique · induction

1.1

The slices. For $b \in B$ put $A_b := A \times \{b\}$ . The map $a \mapsto (a,b)$ is a bijection of $A$ onto $A_b$ , with inverse the first projection, so $A_b$ is finite with $\lvert A_b\rvert = \lvert A\rvert$ ; and the family $(A_b)_{b \in B}$ is pairwise disjoint, since an element of $A_b$ has second coordinate $b$ . Moreover $A \times B = \bigcup_{b \in B} A_b$ .

L2L6construct

1.2

Base case of clause 2, at $m = 0$ . A function with domain $0 = \varnothing$ is the empty function and there is exactly one of them, so $\prod_{i<0} A_i = \{\varnothing\}$ , which is finite with cardinality $1$ because $b \mapsto \varnothing$ is a bijection of $1 = \{0\}$ onto it; and $\prod_{i<0}\lvert A_i\rvert = 1$ by [L5].

baseL2L5L6

1.3

Inductive hypothesis for clause 2: fix $m$ and assume that for every finite list $A_0, \dots, A_{m-1}$ of finite sets the set $\prod_{i<m} A_i$ is finite with cardinality $\prod_{i<m}\lvert A_i\rvert$ .

2.1

Clause 1. By step 1.1 and [L3], $A \times B$ is finite and $\lvert A \times B\rvert = \sum_{b \in B}\lvert A_b\rvert = \sum_{b \in B}\lvert A\rvert = \lvert B\rvert \cdot \lvert A\rvert = \lvert A\rvert \cdot \lvert B\rvert$ , using [L4] for the constant summand and commutativity for the last step.

step 1.1L3L4L7

3.1

Inductive step for clause 2. Let $A_0, \dots, A_m$ be finite. Define $\Phi : \prod_{i<\sigma(m)} A_i \to \big(\prod_{i<m} A_i\big) \times A_m$ by $\Phi(f) = (f\restriction m,\ f(m))$ , where $f \restriction m$ is the restriction of $f$ to $m$ . Its inverse is $(g, a) \mapsto g \cup \{(m,a)\}$ , a function with domain $\sigma(m) = m \cup \{m\}$ because $m \notin m$ ; the two composites are the identity, so $\Phi$ is a bijection. By the hypothesis of step 1.3 and clause 1, the codomain is finite with cardinality $\big(\prod_{i<m}\lvert A_i\rvert\big)\cdot\lvert A_m\rvert = \prod_{i<\sigma(m)}\lvert A_i\rvert$ , and transport carries this to $\prod_{i<\sigma(m)} A_i$ .

step 1.3step 2.1L2L5L6L7

4.1

By step 1.2, step 3.1 and induction, clause 2 holds for every $m \in \mathbb{N}$ .

step 1.2step 3.1L1

5.1

Clause 1 is step 2.1 and clause 2 is step 4.1.

step 2.1step 4.1discharge-induction∎

Remarks

No arithmetic is needed for clause 1. Slicing $A \times B$ over $B$ and applying the sum rule replaces the usual bijection $(p,q) \mapsto p\lvert B\rvert + q$ , which would have to be proved bijective by division with remainder. Division with remainder lives later in the reading order, so the slicing argument is not merely shorter here, it is the one available.
The empty cases are computed. With $A = \varnothing$ and $B$ arbitrary, clause 1 reads $\lvert\varnothing\rvert = 0 \cdot \lvert B\rvert = 0$ , which is right because $\varnothing \times B = \varnothing$ . With $m = 0$ , clause 2 reads $1 = 1$ . Neither is a convention.
The infinite analogue of clause 1 fails in the shape a reader expects. A product of two infinite sets need not be strictly larger than either factor: $\mathbb{N}\times\mathbb{N} \approx \mathbb{N}$ ( $\mathbb{N} \times \mathbb{N} \approx \mathbb{N}$ ). The companion page records that as a false statement, with finiteness located as the hypothesis that fails.

Depends on

Used by

Dependency tree · next 3 levels

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

Rule of product (Wikipedia) (standard reference, not scraped)
Cartesian product (Wikipedia) (standard reference, not scraped)
R. Stanley, Enumerative Combinatorics, Vol. 1, Ch. 1 (standard reference, not scraped)

The product rule: ∣A×B∣=∣A∣ ∣B∣\lvert A \times B\rvert = \lvert A\rvert\,\lvert B\rvert∣A×B∣=∣A∣∣B∣, and ∣∏i<mAi∣=∏i<m∣Ai∣\big\lvert\prod_{i<m} A_i\big\rvert = \prod_{i<m}\lvert A_i\rvert​∏i<m​Ai​​=∏i<m​∣Ai​∣