Alphabeta MathHow 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.
A finite set with has exactly bijections onto itself, and bijections onto any set of the same cardinality
Statement
Let be a finite set with and write
Then is finite and (The factorial and the falling factorial , defined by recursion in ).
More generally, for finite sets and write for the set of bijections . If then is finite with elements, and if then .
Facts & Assumptions
Given: Finite sets , , , with .
, and is finite (The number of injections from a -element set into an -element set is ).
Every injection of a finite set into itself is a bijection (A subset of a finite set is finite, with , and equality holds if and only if , clause 4).
Cardinality (The cardinality of a finite set): a bijection transports finiteness and cardinality, and for finite , one has if and only if .
Maps (Injection, surjection, bijection, Equinumerous sets, and ): composites and inverses of bijections are bijections, and every bijection is an injection.
Proof
The two sets coincide: . Every bijection is an injection, and by [L2] every injection is a bijection, being finite.
Hence is finite with , by [L1] with and by [L3].
The two-set form. Suppose . Then by [L4], so fix a bijection . The map sends into and has the two-sided inverse , so it is a bijection; hence is finite with by step 2.1 and [L4]. If instead then by [L4], so no bijection exists at all.
The first assertion is step 2.1 and the second is step 3.1.
Remarks
-
No group vocabulary is used or needed. is written here as a set of bijections. Composition makes it a group, and that structure, together with the name symmetric group, is introduced in The symmetric group : the bijections of a set under composition ↗ later in the reading order; the pointer is orientation only and nothing above rests on it. The count proved here is what a later page needs in order to say that the symmetric group on letters has elements.
-
Why this is on the main page and not among the examples. Later pages consume this count, and an examples page is a leaf that nothing else may depend on.
-
The two-set form costs one line and is used immediately. The closed formula for counts the bijections between an initial segment and an arbitrary -element subset, which is exactly with .
Depends on
- The number of injections from a $k$-element set into an $n$-element set is $n^{\underline{k}}$
- 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$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- The cardinality $\lvert A\rvert$ of a finite set
- Injection, surjection, bijection
- Equinumerous sets, $A \approx B$ and $A \preceq B$
Used by
- Aₙ is normal in Sₙ; for n≥2, 2 |Aₙ|=n!, while Aₙ=Sₙ for n=0,1 Corollary
- The class equation of Sₙ is n!=∑_∑ k cₖ=n n!/∏ₖ k^cₖcₖ! Corollary
- Two sets of the same finite cardinality between which the bijection is not unique Counterexample
- For n≥1, the determinant over a commutative ring by the Leibniz formula, and |det A| for a real matrix Definition
- The derangement number Dₙ: the number of bijections of an n-element set with no fixed point Definition
- A full 3×3 Leibniz expansion lists all six permutations and their signs Example
- All nine derangements of a four-element set listed, and the count checked against the formula and both recurrences Example
- Hol(C₂× C₂)≅ S₄ Example
- Sym({0,1,2})≅⟨ s,t∣ s², t², (st)³⟩ Example
- The class equation of S₃ is 6=1+2+3 Example
- The six elements of S₃: one-line form, cycle structure, inversions, and sign Example
- FALSE: every finite group is a direct product of cyclic prime-power groups False statement
- If p<q are primes and |G|=pq, then G has a normal subgroup of order q Lemma
- Permutations with a fixed cycle type are counted by the standard factorial denominator Lemma
- The Boolean lattice on an n-element set has n! maximal chains, and exactly k!(n-k)! contain a fixed k-set Lemma
- C(n, k) k! (n-k)! = n! for k ≤ n; hence C(n, k) k! = n^k̲, the quotient n!/(k!(n-k)!) is a natural number, and C(n, k) = C(n, n-k) Theorem
- Erdős-Ko-Rado theorem: for 1≤ k and n≥ 2k, an intersecting family of k-subsets of an n-set has size at most C(n-1, k-1), and a star attains the bound Theorem
- Every group of order 105 has normal Sylow 5- and 7-subgroups and is not simple Theorem
- If [G:H]=n<∞, then Core_G(H) is normal in G, [G:Core_G(H)]∣ n!, and only finitely many subgroups contain H Theorem
- If σ∈ Sₙ has cₖ cycles of length k, then |C_Sₙ(σ)|=∏ₖ₌₁ⁿ k^cₖcₖ! Theorem
- Szele's bound: for every n≥1, some n-vertex tournament has at least n!/2ⁿ⁻¹ Hamilton paths Theorem
- The twelvefold way Theorem
- ι(Dₙ) = ι(n!)∑_i<n+1(-1)ⁱ/ι(i!), with the term at i = 0 equal to 1 and D₀ = 1 Theorem
Dependency tree · two levels
34 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
- Permutation (Wikipedia) (standard reference, not scraped)
- Factorial (Wikipedia) (standard reference, not scraped)
- R. Stanley, Enumerative Combinatorics, Vol. 1, Ch. 1 (standard reference, not scraped)