TheoremStatement: Literature-sourcedProof: 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 set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$

Statement

Let $A$ and $B$ be finite sets and write

$A^{B} := \{\, f : f \text{ is a function } B \to A \,\}.$

Then $A^{B}$ is finite and $\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}$ , the power being the $\mathbb{N}$ -valued exponentiation of Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ .

Both degenerate cases are covered and neither is a stipulation. If $B = \varnothing$ there is exactly one function $B \to A$ , the empty function, so $\lvert A^{\varnothing}\rvert = 1 = \lvert A\rvert^{0}$ even when $A = \varnothing$ . If $A = \varnothing$ and $B \ne \varnothing$ there is no function at all, so $\lvert A^{B}\rvert = 0 = 0^{\lvert B\rvert}$ with $\lvert B\rvert \ge 1$ .

Facts & Assumptions

Given: Finite sets $A$ and $B$ , and $n := \lvert B \rvert$ . Here $A^B$ is the SET of functions $B \to A$ ; it carries no further structure.

[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$ ; $\lvert A\rvert = 0$ exactly when $A = \varnothing$ ; and a bijection transports finiteness and cardinality.

[L3]

The sum rule for two disjoint blocks: $\lvert S \cup T\rvert = \lvert S\rvert + \lvert T\rvert$ (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 1).

[L4]

The product rule: $\lvert X \times Y\rvert = \lvert X\rvert\cdot\lvert Y\rvert$ for finite $X$ , $Y$ (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).

[L5]

Powers (Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ ): $m^{0} = 1$ and $m^{\sigma(n)} = m^{n}\cdot 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.

[L7]

A 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); cancellation in $\mathbb{N}$ : $x + 1 = y + 1$ implies $x = y$ (Addition is cancellative); and $\sigma(n) = n+1$ , $n = \{\,i : i<n\,\}$ (The natural numbers $\mathbb{N}$ (von Neumann), On $\mathbb{N}$ the order is membership: $m < n \iff m \in n$ ).

Proof

technique · induction

1.1

Base case $\lvert B\rvert = 0$ . Then $B = \varnothing$ by [L2], and a function $\varnothing \to A$ is the empty function, of which there is exactly one whatever $A$ is; so $A^{B} = \{\varnothing\}$ , which is finite with cardinality $1$ because $0 \mapsto \varnothing$ is a bijection of $1 = \{0\}$ onto it. And $\lvert A\rvert^{0} = 1$ by [L5].

baseL2L5L6

1.2

Inductive hypothesis: fix $n \in \mathbb{N}$ and assume that for every finite $A$ and every finite $B'$ with $\lvert B'\rvert = n$ the set $A^{B'}$ is finite with $\lvert A^{B'}\rvert = \lvert A\rvert^{n}$ .

2.1

Inductive step. Let $\lvert B\rvert = \sigma(n)$ . Then $B \ne \varnothing$ by [L2], so fix $b \in B$ and put $B' := B \setminus \{b\}$ , which is finite by [L7]. Since $B = B' \cup \{b\}$ with $B' \cap \{b\} = \varnothing$ and $\lvert\{b\}\rvert = 1$ , [L3] gives $\sigma(n) = \lvert B'\rvert + 1$ , hence $\lvert B'\rvert = n$ by cancellation. Define $\Psi : A^{B} \to A^{B'} \times A$ by $\Psi(f) = (f\restriction B',\ f(b))$ ; its inverse is $(g,a) \mapsto g \cup \{(b,a)\}$ , which is a function on $B' \cup \{b\} = B$ because $b \notin B'$ , and the two composites are the identity, so $\Psi$ is a bijection. By the hypothesis of step 1.2 and by [L4] the codomain is finite with cardinality $\lvert A\rvert^{n}\cdot\lvert A\rvert = \lvert A\rvert^{\sigma(n)}$ , and transport carries this to $A^{B}$ .

step 1.2L2L3L4L5L6L7construct

3.1

By induction on $\lvert B\rvert$ the statement holds for every pair of finite sets $A$ , $B$ .

step 1.1step 2.1L1

4.1

The two degenerate readings are instances of it: $B = \varnothing$ gives $1 = \lvert A\rvert^{0}$ by step 1.1, valid for $A = \varnothing$ as well; and $A = \varnothing$ with $\lvert B\rvert \ge 1$ gives $\lvert A^{B}\rvert = 0^{\lvert B\rvert} = 0$ , which is right because a function $B \to \varnothing$ would have to supply a value in $\varnothing$ for some element of $B$ .

step 1.1step 3.1L2L5discharge-induction∎

Remarks

Where the choice of $b$ sits. A single element is taken from a single nonempty set, which is an ordinary existential instantiation and not a choice principle. Nothing in the argument selects a point of every member of a family.
$A^{B}$ here is a bare set. The same set carries a vector space structure over a field in The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = \{0, 1, \dots, n-1\}$ ↗, much later in the reading order; that structure is not used, and this theorem is a count and nothing more.
The exponent notation is not an accident. $\lvert A\rvert^{\lvert B\rvert}$ counts the functions $B \to A$ , and $\lvert A\rvert^{n}$ is by clause (e) of Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $\mathbb{R}$ the product of $n$ copies of $\lvert A\rvert$ : one factor for each element of the domain, which is exactly what the inductive step does one point at a time.

Depends on

Used by

Dependency tree · next 3 levels

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

Exponentiation (Wikipedia) (standard reference, not scraped)
Function (mathematics) (Wikipedia) (standard reference, not scraped)
R. Stanley, Enumerative Combinatorics, Vol. 1, Ch. 1 (standard reference, not scraped)
Twelvefold way (Wikipedia) (standard reference, not scraped)
Power set (Wikipedia) (standard reference, not scraped)

The set ABA^{B}AB of functions B→AB \to AB→A between finite sets is finite, with ∣AB∣=∣A∣∣B∣\lvert A^{B}\rvert = \lvert A\rvert^{\lvert B\rvert}∣AB∣=∣A∣∣B∣