TheoremStatement: AI-adaptedProof: AI-generatedprecheck 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: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$

Statement

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

At $m = 0$ clause 2 reads $∣ \prod_{i < 0} A_{i} ∣ = 1$ : there is exactly one function with domain $\emptyset$ , 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 $σ (m) = m \cup {m}$ and $m = {i : i < m}$ .

[L1]

Induction (The principle of mathematical induction).

[L2]

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

[L3]

The sum rule (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , 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 = ∣ S ∣ \cdot c$ for a constant $c$ .

[L5]

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

[L6]

Maps (Injection, surjection, bijection, Equinumerous sets, $A \approx B$ and $A ⪯ 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}$ , $σ (m) = m \cup {m}$ , $m \notin m$ (On $N$ the order is membership: $m < n ⟺ m \in n$ , The natural numbers $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 $∣ A_{b} ∣ = ∣ A ∣$ ; 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 = ⋃_{b \in B} A_{b}$ .

L2L6construct

1.2

Base case of clause 2, at $m = 0$ . A function with domain $0 = \emptyset$ is the empty function and there is exactly one of them, so $\prod_{i < 0} A_{i} = {\emptyset}$ , which is finite with cardinality $1$ because $b \mapsto \emptyset$ is a bijection of $1 = {0}$ onto it; and $\prod_{i < 0} ∣ A_{i} ∣ = 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} ∣ A_{i} ∣$ .

2.1

Clause 1. By step 1.1 and [L3], $A \times B$ is finite and $∣ A \times B ∣ = \sum_{b \in B} ∣ A_{b} ∣ = \sum_{b \in B} ∣ A ∣ = ∣ B ∣ \cdot ∣ A ∣ = ∣ A ∣ \cdot ∣ B ∣$ , 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 $Φ : \prod_{i < σ (m)} A_{i} \to (\prod_{i < m} A_{i}) \times A_{m}$ by $Φ (f) = (f ↾ m, f (m))$ , where $f ↾ m$ is the restriction of $f$ to $m$ . Its inverse is $(g, a) \mapsto g \cup {(m, a)}$ , a function with domain $σ (m) = m \cup {m}$ because $m \notin m$ ; the two composites are the identity, so $Φ$ is a bijection. By the hypothesis of step 1.3 and clause 1, the codomain is finite with cardinality $(\prod_{i < m} ∣ A_{i} ∣) \cdot ∣ A_{m} ∣ = \prod_{i < σ (m)} ∣ A_{i} ∣$ , and transport carries this to $\prod_{i < σ (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 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 ∣ B ∣ + 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 = \emptyset$ and $B$ arbitrary, clause 1 reads $∣ \emptyset ∣ = 0 \cdot ∣ B ∣ = 0$ , which is right because $\emptyset \times B = \emptyset$ . 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: $N \times N \approx N$ ( $N \times N \approx N$ ). The companion page records that as a false statement, with finiteness located as the hypothesis that fails.

Depends on

Used by

…and 12 more results.

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

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∣∣A×B∣=∣A∣∣B∣, and ∣∏i<mAi∣=∏i<m∣Ai∣​∏i<m​Ai​​=∏i<m​∣Ai​∣