LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

$\sum_{i \in S}\sum_{j \in T} a_{ij} = \sum_{(i,j) \in S \times T} a_{ij} = \sum_{j \in T}\sum_{i \in S} a_{ij}$ for finite index sets $S$ and $T$

Statement

Let $S$ and $T$ be finite sets and let $a : S \times T \to \mathbb{R}$ , or $a : S \times T \to \mathbb{N}$ , written $a_{ij}$ for $a(i,j)$ . Then $S \times T$ is finite and

$\sum_{i \in S}\Big(\sum_{j \in T} a_{ij}\Big) \;=\; \sum_{p \in S \times T} a_p \;=\; \sum_{j \in T}\Big(\sum_{i \in S} a_{ij}\Big),$

all three sums being the sums over a finite index set of The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form, carried by Finite sums and finite products, by recursion when the values are real and by Finite sums and finite products of natural numbers, $\sum_{k<n} a_k$ and $\prod_{k<n} a_k$ in $\mathbb{N}$ when they are natural.

This is not a clause of 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. That theorem splits one sum along a partition of its own index set; the identity above exchanges the roles of two different index sets, and it is what an argument that counts a set of pairs in two ways needs. Both outer index sets may be empty, in which case all three quantities are $0$ (respectively $1$ for the product form of the underlying recursion), since a sum over the empty index set is the empty sum.

Facts & Assumptions

Given: Finite sets $S$ and $T$ , and a list $a$ defined on $S \times T$ with values in $\mathbb{R}$ or in $\mathbb{N}$ .

[L1]

$S \times T$ is finite (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$ , clause 1), and every subset of a finite set is finite (A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$ , and equality holds if and only if $B = A$ , clause 1).

[L2]

Splitting along a partition: if $P$ is finite, $J$ is finite, and $(P_j)_{j \in J}$ are pairwise disjoint subsets of $P$ whose union is $P$ , then $\sum_{p \in P} a_p = \sum_{j \in J}\big(\sum_{p \in P_j} a_p\big)$ , for real-valued and for natural-valued $a$ alike (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, clause 3).

[L3]

Reindexing along a bijection: if $h : V \to P$ is a bijection of finite sets then $\sum_{v \in V} a_{h(v)} = \sum_{p \in P} a_p$ (The sum $\sum_{i \in S} a_i$ over a finite index set, and its product form, clause (b)).

[L4]

A map with a two-sided inverse is a bijection (Injection, surjection, bijection).

Proof

technique · direct

1.1

The row slices. For $i \in S$ put $P_i := \{i\} \times T$ . Each $P_i$ is a subset of the finite set $S \times T$ , hence finite; the family $(P_i)_{i \in S}$ is pairwise disjoint, because a point of $P_i$ has first coordinate $i$ ; and its union is $S \times T$ , because every $p \in S \times T$ is $(i,j)$ for some $i \in S$ and $j \in T$ .

L1construct

1.2

The column slices. For $j \in T$ put $Q_j := S \times \{j\}$ . The same three observations with the coordinates exchanged show that each $Q_j$ is finite, that the family $(Q_j)_{j \in T}$ is pairwise disjoint, and that its union is $S \times T$ .

L1construct

1.3

The slice bijections. For $i \in S$ the map $h_i : T \to P_i$ , $h_i(j) := (i,j)$ , takes its values in $P_i$ by definition and has the second-coordinate map as a two-sided inverse, so it is a bijection; likewise $g_j : S \to Q_j$ , $g_j(i) := (i,j)$ , is a bijection for each $j \in T$ .

L3L4construct

2.1

Splitting the sum over $S \times T$ along the row slices gives $\sum_{p \in S \times T} a_p = \sum_{i \in S}\big(\sum_{p \in P_i} a_p\big)$ .

step 1.1L2

2.2

Splitting it along the column slices gives $\sum_{p \in S \times T} a_p = \sum_{j \in T}\big(\sum_{p \in Q_j} a_p\big)$ .

step 1.2L2

2.3

Reindexing each inner sum along the bijection of step 1.3 gives $\sum_{p \in P_i} a_p = \sum_{j \in T} a_{h_i(j)} = \sum_{j \in T} a_{ij}$ for every $i \in S$ , and $\sum_{p \in Q_j} a_p = \sum_{i \in S} a_{ij}$ for every $j \in T$ .

step 1.3L3

3.1

Substituting step 2.3 into step 2.1 and into step 2.2 gives $\sum_{i \in S}\big(\sum_{j \in T} a_{ij}\big) = \sum_{p \in S \times T} a_p = \sum_{j \in T}\big(\sum_{i \in S} a_{ij}\big)$ , which is the statement.

step 2.1step 2.2step 2.3∎

Remarks

What is actually used. Only the splitting clause and the reindexing clause, and each of them is stated for a real-valued and for a natural-valued summand. One argument therefore proves both readings, and nothing about subtraction or about the order enters.
Why the slices and not an induction. The two partitions of $S \times T$ are the same set cut two ways, so the identity is a statement about one sum, not a statement relating two recursions. That is why no induction appears and why the empty cases need no separate treatment: a sum over an empty index set is the empty sum, and the argument passes through it unchanged.

Depends on

Used by

Dependency tree · next 3 levels

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

Summation (Wikipedia) (standard reference, not scraped)
Double counting (proof technique) (Wikipedia) (standard reference, not scraped)
R. Stanley, Enumerative Combinatorics, Vol. 1, Ch. 1 (standard reference, not scraped)
Mathematics for Computer Science (MIT OpenCourseWare) (standard reference, not scraped)

∑i∈S∑j∈Taij=∑(i,j)∈S×Taij=∑j∈T∑i∈Saij\sum_{i \in S}\sum_{j \in T} a_{ij} = \sum_{(i,j) \in S \times T} a_{ij} = \sum_{j \in T}\sum_{i \in S} a_{ij}∑i∈S​∑j∈T​aij​=∑(i,j)∈S×T​aij​=∑j∈T​∑i∈S​aij​ for finite index sets SSS and TTT