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.
Inclusion–Exclusion, the Pigeonhole Principle and Double Counting
1 · Prerequisites
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Relations, Functions, and Quotients
- Roots, Rational Powers, and Classical Inequalities
- The ZFC Axioms and the Basic Set Constructions
2 · Summary
Finite cardinality, finite sums over arbitrary finite index sets, the sum and product rules, binomial coefficients, and the canonical embedding of the naturals into the reals supply the counting and arithmetic background. The alternating binomial-row identity controls signed subset sums, while ordered-field arithmetic permits subtraction and division after natural counts are embedded in . A finite incidence relation supplies row and column fibres, and a finite family of subsets of a named ambient set supplies its intersections, including the empty intersection relative to that ambient set.
Counting a finite incidence relation by either fibre family yields double counting and the averaging principle; applying the same partition-of-fibres argument to a function gives the strong pigeonhole principle and its ceiling form. Pointwise alternating sums over traces give inclusion-exclusion, and partial binomial-row sums give the Bonferroni bounds. Sieving functions by omitted values counts surjections, while sieving permutations by fixed points gives the derangement formula and its recurrences. Finally, longest increasing and decreasing sublists ending at each position define an injective rank-pair map, proving the Erdős–Szekeres bound; decreasing blocks ordered increasingly supply the sharp examples of length .
3 · Logical flowchart
4 · Definitions, theorems and proofs
for finite index sets and
Statement
Let and be finite sets and let , or , written for . Then is finite and
all three sums being the sums over a finite index set of The sum 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, and in when they are natural.
This is not a clause of The sum rule: a finite disjoint union is finite with and , 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 (respectively 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 and , and a list defined on with values in or in .
is finite (The product rule: , and , clause 1), and every subset of a finite set is finite (A subset of a finite set is finite, with , and equality holds if and only if , clause 1).
Splitting along a partition: if is finite, is finite, and are pairwise disjoint subsets of whose union is , then , for real-valued and for natural-valued alike (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 3).
Reindexing along a bijection: if is a bijection of finite sets then (The sum over a finite index set, and its product form, clause (b)).
A map with a two-sided inverse is a bijection (Injection, surjection, bijection).
Proof
The row slices. For put . Each is a subset of the finite set , hence finite; the family is pairwise disjoint, because a point of has first coordinate ; and its union is , because every is for some and .
The column slices. For put . The same three observations with the coordinates exchanged show that each is finite, that the family is pairwise disjoint, and that its union is .
The slice bijections. For the map , , takes its values in by definition and has the second-coordinate map as a two-sided inverse, so it is a bijection; likewise , , is a bijection for each .
Splitting the sum over along the row slices gives .
Splitting it along the column slices gives .
Reindexing each inner sum along the bijection of step 1.3 gives for every , and for every .
Substituting step 2.3 into step 2.1 and into step 2.2 gives , which is the statement.
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 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.
A relation between finite sets, its row fibres and its column fibres
Definition
Let and be finite sets (Finite, countably infinite, countable, uncountable, The cardinality of a finite set) and let be a relation between them. For and set
the row fibre of at and the column fibre of at .
(a) Everything here is finite. is finite (The product rule: , and , clause 1), so is finite as a subset of it, and and are finite as subsets of finite sets (A subset of a finite set is finite, with , and equality holds if and only if , clause 1). Hence , and are all defined, and each is a natural number (The cardinality of a finite set).
(b) The fibres are the slices of , up to a bijection. For ,
since lies in the left-hand side exactly when , and , that is exactly when and . The map is a bijection of onto , its two-sided inverse being the second-coordinate map (Injection, surjection, bijection), so by the transport clause (c) of The cardinality of a finite set. Symmetrically and .
(c) The slices partition . The sets , for , are pairwise disjoint, because a point of has first coordinate ; and their union is , because every has and . Symmetrically the sets , for , are pairwise disjoint with union .
(d) Neighbours. When and is symmetric ( implies ) and irreflexive ( for every ), and this common set is called the set of neighbours of ; it is a subset of .
Remarks
-
A relation, not a matrix. The object counted here is a subset of a product of two finite sets. Nothing about arrays, entries or indices by position is used, and the two fibre families are the only structure the counting arguments need.
-
No graph vocabulary. Clause (d) fixes the words symmetric, irreflexive and neighbour for a relation on a single finite set. Nothing among this page's declared prerequisites defines a graph, and none of the results stated with clause (d) needs one.
-
Both fibre families are indexed by a finite set, which is what lets the cardinalities be summed at all: a sum over a finite index set is defined only when the index set is finite (The sum over a finite index set, and its product form).
Double counting: for a relation between finite sets
Statement
Let and be finite sets and let , with row fibres and column fibres as in A relation between finite sets, its row fibres and its column fibres . Then, in ,
the sums being those of The sum over a finite index set, and its product form.
Both index sets may be empty. If then , every column fibre is empty, and all three quantities are ; the same holds with the roles of and exchanged.
Facts & Assumptions
Given: Finite sets and , a relation , and its fibres.
, every and every are finite, so all the cardinalities written below are defined (A relation between finite sets, its row fibres and its column fibres , clause (a), The cardinality of a finite set).
The row slices and column slices are pairwise disjoint within their respective families and each family has union by clause (c); they are finite because clause (b) bijects them with the finite fibres from [L1] (A relation between finite sets, its row fibres and its column fibres , clauses (b) and (c), The cardinality of a finite set, clause (c)).
and , by the slice bijections of clause (b) of A relation between finite sets, its row fibres and its column fibres and the transport clause (c) of The cardinality of a finite set (Injection, surjection, bijection).
The sum rule for a finite partition: if is a family of pairwise disjoint finite sets indexed by a finite set , then is finite with (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 2, The sum over a finite index set, and its product form).
Proof
The row slices form a family of pairwise disjoint finite sets indexed by the finite set , and their union is , so [L4] gives .
The column slices form a family of pairwise disjoint finite sets indexed by the finite set , and their union is , so [L4] gives .
Replacing each summand of step 1.1 by and each summand of step 1.2 by , which is legitimate by [L3] since the two lists have the same values at every index, gives .
Remarks
-
Where the hypotheses are spent. Finiteness of and of is what makes the two index sets legitimate index sets for a sum, and finiteness of is what makes defined. Disjointness of the slices is automatic, since a slice is determined by one coordinate of its points, which is why no hypothesis of that kind appears in the statement.
-
The count stays in . Every quantity here is a cardinality, and the sums are the -valued ones. Nothing is embedded into until an identity with a subtraction or a division has to be written.
If is nonempty, some row fibre is at least the average size and some row fibre is at most the average size
Statement
Let and be finite sets with , let , and let be its row fibres (A relation between finite sets, its row fibres and its column fibres ). Since , the real number
is defined, where is the canonical natural (The canonical natural of a field). Then there are with
The two elements need not be distinct, and neither inequality need be an equality: is a real number and a fibre size is a natural number, so no fibre need meet the average exactly.
Facts & Assumptions
Given: Finite sets and , a relation with row fibres , and a fixed enumeration of , which exists because is finite (The cardinality of a finite set).
Double counting: in (Double counting: for a relation between finite sets).
The bridge over a finite index set: for a finite and , . This is not a clause of The sum over a finite index set, and its product form and is derived here: both sides are computed through one and the same enumeration , and is clause 6 of Laws of finite sums and products in , and .
A constant real summand: for (The sum over a finite index set, and its product form, clause (c)).
Additivity and the vanishing test over a finite index set: for one has ; and if for every and , then for every . Both are clauses 1 and 4 of Laws of finite sums and finite products applied to the list through an enumeration of (The sum over a finite index set, and its product form, Finite sums and finite products, by recursion); for the second, is onto , so every value of is some .
is strictly increasing with , so gives (Laws of finite sums and products in , and , clause 7, The canonical natural of a field).
if and only if (The cardinality of a finite set, clause (b)).
is an ordered field: its order is total, a nonzero element has a multiplicative inverse, and is equivalent to (Ordered field, Field).
Proof
Since , [L6] gives , hence and by [L5]; in particular , so names a single real number and .
Applying [L2] to the list and then [L1] gives .
A positive list over a nonempty finite index set has nonzero sum: if has for every and , then for every , so [L4] forces for every ; as has an element, its value is then both and positive, which is impossible.
By [L3] with the constant , , the second equality by step 1.1.
Suppose there were no with . Since the order of is total, for every , so is positive for every ; and by additivity, step 1.2 and step 2.1, , that is , contradicting step 1.3. So some has .
Suppose there were no with . Then for every , so is positive for every ; the same computation gives , again contradicting step 1.3. So some has .
Steps 3.1 and 3.2 are the two assertions of the statement.
Remarks
-
Why is a hypothesis and not decoration. It is used twice: to make invertible, so that exists at all, and to produce the element at which the vanishing test is contradicted. With there is no fibre to exhibit and no quotient to compare it to.
-
The average lives in and the fibre sizes live in . A quotient of two natural numbers is not in general a natural number, so the comparison has to be made after both sides are carried into by . This is the reason the statement is written with throughout rather than as , which is not an inequality between elements of one ordered set.
-
Nothing is claimed about attainment. The proof produces an and an and no more; a relation whose fibre sizes all differ from exists, and it is exhibited on the companion page.
for naturals and : the least with
Definition
Let with (The natural numbers (von Neumann), Order on the natural numbers, On the order is membership: ), and put
the multiplication being that of (Multiplication of natural numbers).
is nonempty, so the definition below has something to pick from. Since , Every nonzero natural number is a successor gives for some , and then by the successor-left law of Distributivity and the successor law for multiplication and the commutativity of addition (Addition is commutative), so by the definition of the order (Order on the natural numbers), which asks for a natural with and is met by . Hence .
Definition. is the least element of , which exists by the well-ordering principle (The well-ordering principle) applied to the nonempty subset of . It is a natural number, and it is defined for only.
Four clauses, recorded here because they are what the notation is used for.
(a) . This is membership of in .
(b) Minimality. If satisfies then ; equivalently, every with satisfies , by trichotomy (Trichotomy of the order on ).
(c) Two values read off directly. , since makes the least element of that qualifies; and , since while forces (Zero and one under multiplication, Multiplication is commutative).
(d) The reading in . With the canonical natural (The canonical natural of a field), clause (a) gives by the multiplicativity of (clause 0 of Laws of finite sums and products in , and ) and its strict monotonicity (clause 7); and because . Since is an ordered field (Ordered field, Field), dividing by gives
Remarks
-
This is not a floor and it is not a ceiling function. It is defined for a pair of natural numbers with , its value is a natural number, and it is fixed by one order property and one minimality property. It is not defined for a real argument, it does not extend to negative numbers, and it carries no division: the symbol inside the brackets is part of the notation and not an operation performed anywhere above.
-
Why it is introduced at all. The strong form of the pigeonhole principle says that some fibre has at least "the average, rounded up" elements, and that phrase needs a name for the rounding. The least with is exactly what the proof produces, and the well-ordering principle is exactly what makes it exist, so nothing stronger is required.
-
Nothing among this page's declared prerequisites supplies a division with remainder, and the definition above deliberately does not attempt one: no with and is produced or claimed here.
If then every has a fibre with more than elements, and for nonempty some fibre has at least elements
Statement
Let and be finite sets, let , let , and for write
for the fibre of over (Injection, surjection, bijection). Then:
- The counting form. If then there is with .
- The ceiling form. If then there is with ( for naturals and : the least with , which is defined because ).
Every quantity here is a natural number and the comparisons are those of (Order on the natural numbers). Clause 1 at says that a nonempty has a nonempty fibre. Clause 1 is vacuous when , since then , the hypothesis says , and there is no function from a nonempty set to for the conclusion to be about. Clause 2 at says only that some fibre has at least elements, since .
Facts & Assumptions
Given: Finite sets and , a natural number , a function , and the fibres for .
The fibres are pairwise disjoint subsets of whose union is : distinct values of give disjoint fibres, and every lies in the fibre over . Each fibre is finite (A subset of a finite set is finite, with , and equality holds if and only if , clause 1), so The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition clause 2 gives in (The sum over a finite index set, and its product form, The cardinality of a finite set).
Monotonicity over a finite index set: if satisfy for every , then . Both sums are computed through one enumeration (The sum over a finite index set, and its product form), and for every , so clause 4 of Laws of finite sums and products in , and applies (Finite sums and finite products, by recursion).
A constant natural summand: (The sum over a finite index set, and its product form, clause (c)).
Order and arithmetic of : multiplication is commutative (Multiplication is commutative); exactly one of , , holds (Trichotomy of the order on ); if and only if (Discreteness: is the immediate successor); every nonzero natural is a successor (Every nonzero natural number is a successor); and for every (Order on the natural numbers).
The ceiling ( for naturals and : the least with ): for , is the least with , so any satisfies .
if and only if (The cardinality of a finite set, clause (b)).
Proof
Suppose, for contradiction, that and yet for every .
By [L1], .
For clause 2, assume ; then by [L6], so and is defined, and has at least one element.
Clause 1. Under the assumption of step 1.1, monotonicity and the constant sum give , which contradicts by trichotomy. So the supposition of step 1.1 is untenable and clause 1 holds.
Clause 2 when . Choose any , available by step 1.3; then by [L4].
Clause 2 when . Write by [L4]. Then , so [L5] gives , that is by commutativity; clause 1, established in step 2.1, therefore produces with , and by [L4].
Clause 1 is step 2.1, and clause 2 is steps 2.2 and 3.1, whose two cases are exhaustive.
Remarks
-
Where the ceiling earns its keep. Clause 2 is not a separate argument: it is clause 1 applied at the single value with , and the only thing that has to be checked is that this satisfies , which is exactly the minimality of . That is the whole reason the ceiling was defined by minimality rather than by a division.
-
The case is not a degenerate nuisance. It occurs precisely when , where the conclusion is empty of content but still needs an element of to be stated about, and that is where is spent in clause 2.
-
Disjointness of the fibres is free, since a fibre is determined by the value it lies over. This is what lets the sum rule be applied with no hypothesis beyond finiteness, in contrast to a union of arbitrary sets.
A finite family of subsets of a finite set , the intersections for , and the convention
Definition
A sieve family consists of a finite set , called the ambient set, a finite set , called the index set, and a family of subsets of , that is a function (Finite, countably infinite, countable, uncountable, The cardinality of a finite set). For set
and write for the union of the family.
Why the ambient set has to be named, and why is a stipulation. For the intersection is the set of elements belonging to every with , and it is determined by the family alone. For that description is satisfied by every set whatsoever, so it determines nothing; an intersection of no subsets of is only relative to . Naming as part of the data and stipulating is what makes the symbol defined for all , which is what the complementary form of the sieve identity requires.
(a) Every is a finite subset of . For pick ; then . For , . In both cases is finite by clause 1 of A subset of a finite set is finite, with , and equality holds if and only if , and so is ; hence and are natural numbers (The cardinality of a finite set).
(b) The index sets of the sieve's sums are finite. is finite with ( for finite ); the set of nonempty subsets of and the set of -element subsets of are subsets of , hence finite (A subset of a finite set is finite, with , and equality holds if and only if ), and (The set of -element subsets and the binomial coefficient ).
(c) Monotonicity. If then . For this is clause (a); otherwise an element lying in every with lies in every with .
(d) The trace of a point. For put
a finite set. For every nonempty ,
both sides saying that for every . And if and only if . Writing , clause (b) applied to gives , and for nonempty the condition with says exactly that .
Remarks
-
The counts stay in ; the identities do not. Each is a natural number. Every identity that sieves them carries a minus sign, and has no subtraction, so those identities are stated in through the canonical natural and read back by its injectivity. That is a property of the identities, not of this definition, which introduces no arithmetic at all.
-
is an arbitrary finite index set, not a natural number. Nothing below numbers the sets ; the subsets are the objects the sums run over, and rather than any position is what carries the sign.
-
The clause supplies every empty-subfamily term. In the complementary form at it contributes ; later sieve instances also use it when identifying the intersection at the empty subfamily. Removing the stipulation would leave those terms undefined.
Inclusion and exclusion: , together with the complementary form counting the elements in none of the
Statement
Let , , and the intersections be a sieve family (A finite family of subsets of a finite set , the intersections for , and the convention ), let , and let be the canonical natural (The canonical natural of a field). Then, in :
- The sieve identity. the sum being over the finite index set of nonempty subsets of .
- The complementary form. the sum now being over all subsets of , its term at being by the stipulation .
The identities are stated in because their terms carry signs and has no subtraction; every cardinality appearing is a natural number carried into by , and is injective, so an identity between two of them may be read back in (Laws of finite sums and products in , and , clause 7).
Both readings at are part of the statement. Then and clause 1 reads , the index set of its sum being empty. Clause 2 reads , its sum having the single term at . At the sign in clause 1 is and , so the singleton terms enter with a plus sign.
Facts & Assumptions
Given: A sieve family , , with intersections , union , traces and , all as in A finite family of subsets of a finite set , the intersections for , and the convention ; the abbreviation ; and, for , the indicator with for and otherwise.
Sieve facts (A finite family of subsets of a finite set , the intersections for , and the convention ): , , each , each , and each are finite ( for finite , A subset of a finite set is finite, with , and equality holds if and only if , The cardinality of a finite set); for nonempty , if and only if ; if and only if ; and (The set of -element subsets and the binomial coefficient ).
Splitting a sum along a partition of its index set, and the sum rule for two disjoint blocks (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clauses 3 and 1).
Sums over a finite index set (The sum over a finite index set, and its product form): the value is independent of the enumeration used; (clause (a)); a sum over is and a constant real summand gives (clause (c)).
Interchange of a double sum over two finite index sets ( for finite index sets and ).
Additivity and scaling of a real finite sum over a finite index set: and . Both are clauses 1 and 2 of Laws of finite sums and finite products read through an enumeration of (The sum over a finite index set, and its product form, Finite sums and finite products, by recursion).
Partition of a power set by cardinality: for a finite with , the sets for are pairwise disjoint with union , since a subset of has exactly one cardinality and that cardinality is at most (A subset of a finite set is finite, with , and equality holds if and only if , clause 2).
Powers of and the alternating row sum: and (Integer powers ); and for every (, and for , clause 2). The hypothesis there is not decoration: at that sum is .
is additive and injective (Laws of finite sums and products in , and , clauses 0 and 7), and is an ordered field, so subtraction is available (Ordered field, Field).
Proof
Indicator sums. For every one has : the sets and are disjoint finite sets with union , so [L2] splits the sum into , which is by the constant clause of [L3].
The double list. Define by ; both and are finite by [L1], so both iterated sums of are defined.
Fix and write . The sets and are disjoint with union ; by [L1] we have for and for , so splitting by [L2] gives , and .
Grouping the subsets of by size. By [L6] applied to , then the constant clause of [L3] on each block, then scaling by and from [L7],
Splitting off the empty subset. and are disjoint with union , so [L2] and [L7] give .
The inner sum is the indicator of . If then [L7] makes the right-hand side of step 1.4 zero, so step 1.5 gives . If then , so and that sum is by [L3]. Since exactly when by [L1], step 1.3 gives for every .
The outer sum recovers the sieve terms. Scaling by the constant and applying step 1.1 to gives for every .
Clause 1. Summing step 2.2 over , interchanging by [L4], and then using step 2.1 and step 1.1 with :
Clause 2. The sets and are disjoint finite sets with union , so by [L2] and hence by the additivity of in [L8]. On the other side, and are disjoint with union , so [L2], [L3] and [L7] give , which by step 3.1 is . The two right-hand sides agree, which is clause 2.
Remarks
-
Where the alternating row sum is spent, and why its hypothesis matters. The whole content of the proof is that each contributes to the right-hand side when it lies in some and otherwise. The first case is the vanishing of the full alternating row sum of , which holds only for ; the second case is not that identity at all but the emptiness of the index set. Applying the identity at would give , not , and would make the theorem false.
-
The empty intersection is used once. Only in clause 2, at the term , where contributes . Clause 1 never mentions it.
-
No choice principle is used. A sum over a finite index set is defined because all its enumerations agree, not by selecting one, and the family is given as a function.
for every and every
Statement
Let with and let . Then, in ,
where is the canonical natural (The canonical natural of a field), the binomial coefficients are the counts of The set of -element subsets and the binomial coefficient , and is the truncated difference of Finite sums and finite products of natural numbers, and in , which for is the ordinary one, so that .
The hypothesis is part of the statement. At and the left-hand side is , while the truncated difference gives and the right-hand side is .
Two readings worth recording. At both sides are , since . For both sides are : the terms of the left-hand side with vanish and the remaining sum is the full alternating row sum of , which vanishes because , while because .
Facts & Assumptions
Given: Naturals and ; the abbreviation , so that (Finite sums and finite products of natural numbers, and in , Order on the natural numbers); the real finite sum of Finite sums and finite products, by recursion; and integer powers (Integer powers ) in the ordered field (Ordered field, Field).
Induction: a property holding at and inherited by successors holds at every natural (The principle of mathematical induction).
Recursion clauses of the real finite sum: and (Finite sums and finite products, by recursion, Laws of finite sums and finite products).
Pascal's rule, with no restriction relating the two indices: for all (Pascal's rule , and the hockey-stick identity , clause 1).
for every (The set of -element subsets and the binomial coefficient ); and is additive (Laws of finite sums and products in , and , clause 0, The canonical natural of a field).
Powers of : and (Integer powers ).
Proof
Fix and write , so that ; the claim is proved by induction on , for this fixed .
Base case . By [L2] the left-hand side is the single term , which is by [L4] and [L5]; and the right-hand side is for the same reason.
Inductive hypothesis: fix and assume .
Pascal's rule at and , together with , gives , hence by the additivity of .
By the recursion clause of [L2] and the hypothesis of step 1.3, .
Substituting step 1.4 into step 2.1 and using from [L5]: .
So the claim holds at whenever it holds at , and it holds at ; by [L1] it holds for every , for the fixed , which was arbitrary.
Remarks
-
Where is spent. In exactly one place: the identity , which is what lets Pascal's rule be applied with upper index . Under the truncated difference the equation fails at , where and , and the statement fails there too.
-
Why not the full alternating row sum. The published corollary of the binomial theorem gives the sum over the whole row, and only for . A truncation of that row is a different quantity, and the identity above is what says how far a truncation misses: by exactly one binomial coefficient of the row above, with the sign of the last term kept.
Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it
Statement
Let , , and the intersections be a sieve family (A finite family of subsets of a finite set , the intersections for , and the convention ), let , put , and let be the canonical natural (The canonical natural of a field). For and set
the first sum being over the finite set of -element subsets of and the second the real finite sum of Finite sums and finite products, by recursion. Thus , and . Then, in :
- Odd truncation over-estimates. for every .
- Even truncation under-estimates. for every .
- Both are equalities once the truncation reaches . for every .
Clause 1 at is the union bound , and clause 2 at is the trivial ; the first substantial even case is , where .
Facts & Assumptions
Given: A sieve family , , with intersections , union , traces and (A finite family of subsets of a finite set , the intersections for , and the convention ); ; the quantities and of the Statement; and, for , the indicator with value on and off it.
Indicator sums: for a finite and . Split into the disjoint blocks and (clause 3 of The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition) and apply the constant clause (c) of The sum over a finite index set, and its product form.
Sieve facts (A finite family of subsets of a finite set , the intersections for , and the convention ): , , , and are finite ( for finite , A subset of a finite set is finite, with , and equality holds if and only if , The cardinality of a finite set); for nonempty , if and only if ; if and only if ; (The set of -element subsets and the binomial coefficient ); and every satisfies , by clause 2 of A subset of a finite set is finite, with , and equality holds if and only if , so whenever .
Splitting a sum along a partition of its index set (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 3); and, for sums over a finite index set, the bridge , the empty index set and the constant summand (The sum over a finite index set, and its product form, clauses (a) and (c)).
Interchange of a double sum over two finite index sets ( for finite index sets and ).
Real finite-sum laws, read over a finite index set through an enumeration (The sum over a finite index set, and its product form): additivity, scaling, splitting at an index and monotonicity (Laws of finite sums and finite products, clauses 1 to 4, Finite sums and finite products, by recursion).
The partial alternating row sum: for every and every ( for every and every ).
Powers of : and (Integer powers ); and , . For the last two, by clause 1 of Laws of integer exponents, and by clauses (b) and (d) of Exponentiation of natural numbers, , and its agreement with the integer power in with The canonical natural of a field; then .
Inclusion and exclusion, clause 1 (Inclusion and exclusion: , together with the complementary form counting the elements in none of the ).
Boundary values of a binomial coefficient: for every , while whenever , so in particular for (The set of -element subsets and the binomial coefficient ); and for every natural , being strictly increasing with (Laws of finite sums and products in , and , clause 7).
is an ordered field (Ordered field, Field).
Proof
Each with counted pointwise. By [L1], for every ; interchanging the resulting double sum by [L4] gives . For every is nonempty, so by [L2] the inner sum is of the number of with , that is . Hence for every .
The pointwise truncation. For and put .
A closed form for . Splitting at the index by [L5] gives , which by [L7] and scaling is ; hence . So when , by [L6]. When every term of is by [L9], so .
counted pointwise. Scaling step 1.1 by gives for every ; summing over , using from [L3] and interchanging by [L4], gives for every .
The pointwise comparison. Let and . If then by [L2], so by step 1.3. If then , and step 1.3 with [L7] gives and , since of a natural number is at least by [L9]. So for every .
Clauses 1 and 2. Monotonicity of a finite sum over the index set , applied to step 2.2, gives ; the middle term is by [L1] and the outer two are and by step 2.1.
Clause 3. The sets for are pairwise disjoint with union , since a nonempty has exactly one cardinality and it satisfies by [L2]; splitting the sieve sum along this partition, and using for from [L7], gives , which equals by [L8]. For , splitting at the index by [L5] and noting that forces , hence and by [L2], [L3] and [L9], gives ; with step 3.1 this completes all three clauses.
Remarks
-
Why the parity is written as and . Nothing among this page's declared prerequisites defines the words even and odd, and the statement needs only the two families of truncation depths, which the two displayed forms name directly. The sign facts and are then the whole use of parity in the proof.
-
Where the error term comes from. Step 1.3 says that a truncation at depth misses the indicator of at a point of trace size by exactly , a single binomial coefficient. The sign of that term is what makes the inequality go one way for one parity and the other way for the other, and its nonnegativity is what makes the inequality hold at all.
-
A point outside the union contributes nothing at any depth, which is why no hypothesis relating to appears. The ambient set may be much larger than the union without affecting either side.
The number of surjections from an -element set onto a -element set is , read in through
Statement
Let and be finite sets, and , and write
(Injection, surjection, bijection). Then is finite and, in ,
where is the canonical natural (The canonical natural of a field), is the -valued power of Exponentiation of natural numbers, , and its agreement with the integer power in , and is the truncated difference of Finite sums and finite products of natural numbers, and in , which is the ordinary one throughout the range of the sum.
All three degenerate readings are part of the statement, and each is computed rather than stipulated.
- and . There is exactly one function , the empty function, and it is a surjection, so the count is . The sum has the single term , and is the base clause of Exponentiation of natural numbers, , and its agreement with the integer power in , so the sum is too.
- and . No function is a surjection, so the count is ; and every factor is , so the sum is the full alternating row sum , which is because (, and for , clause 2).
- and . There is no function from a nonempty set to , so the count is ; and the sum has the single term , which is because (Exponentiation of natural numbers, , and its agreement with the integer power in , clause (a)).
Facts & Assumptions
Given: Finite sets and with and ; the set of all functions ; and, for , the set of functions missing the value .
is finite with . This is The set of functions between finite sets is finite, with with its taken to be and its taken to be , so that its is the set of functions and its formula reads (Exponentiation of natural numbers, , and its agreement with the integer power in ).
is a family of subsets of the finite set indexed by the finite set , hence a sieve family with ambient set , and its intersections for satisfy (A finite family of subsets of a finite set , the intersections for , and the convention , A subset of a finite set is finite, with , and equality holds if and only if , The cardinality of a finite set).
is a surjection exactly when , that is exactly when there is no with (Injection, surjection, bijection). Hence , and it is finite as a subset of (A subset of a finite set is finite, with , and equality holds if and only if ).
For a finite sieve family in with , the complementary identity is (Inclusion and exclusion: , together with the complementary form counting the elements in none of the , clause 2).
For : , so (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 1, and the truncated difference of Finite sums and finite products of natural numbers, and in ).
Partition of a power set by cardinality: the sets for are pairwise disjoint with union , since a subset of has exactly one cardinality and it is at most ; and (A subset of a finite set is finite, with , and equality holds if and only if , clause 2, The set of -element subsets and the binomial coefficient , for finite ).
Splitting a sum along a partition of its index set (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 3); a constant real summand and the bridge (The sum over a finite index set, and its product form, clauses (a) and (c)); and the real finite sum itself (Finite sums and finite products, by recursion).
is injective and (Laws of finite sums and products in , and , clause 7, Integer powers ).
Proof
The ambient set. Put ; it is finite with by [L1].
The sieve family. For the set of functions missing is a subset of , and by [L3] a function is a surjection exactly when ; so is the complement of the union of the sieve family inside .
The intersections are function sets. For every , : for , says that misses every , that is that takes all its values in ; and for both sides are , the left by the stipulation of [L2]. Hence by [L1] applied to and by [L5].
The sieve. Applying [L4] to the family of step 1.2 and substituting step 1.3, .
Grouping the subsets of by size. Splitting the last sum along the partition of [L6] and using the constant clause of [L7] on each block, where the summand depends on only through , gives .
Combining steps 2.1 and 3.1 gives , and is finite by [L3]; since is injective, the identity determines the count in .
Remarks
-
The convention is load bearing exactly once, at and , where the formula returns and the truth is that the empty function is a surjection onto the empty set. It is not a convenience: it is the base clause of the recursion defining natural exponentiation, and changing it would make the formula false at that single point.
-
Why the family is indexed by and not by . The sieve removes the functions that miss a value, and there is one condition per element of the codomain. This is also why the alternating sum runs to and not to .
-
The count is a natural number. The identity is stated in because it carries signs, and is injective, so it pins down the natural number exactly.
The derangement number : the number of bijections of an -element set with no fixed point
Definition
Let be a finite set. A derangement of is a bijection with for every (Injection, surjection, bijection). Write
where is the set of bijections of onto itself.
is finite. is finite with (A finite set with has exactly bijections onto itself, and bijections onto any set of the same cardinality, The factorial and the falling factorial , defined by recursion in ), and is a subset of it, hence finite (A subset of a finite set is finite, with , and equality holds if and only if , clause 1). So is a natural number (The cardinality of a finite set).
The count depends only on . Let be a bijection of finite sets. The map sends into , since composites and inverses of bijections are bijections, and it sends into : if for some then, applying and writing , we get . The map is a two-sided inverse, so and the two sets have the same cardinality by the transport clause (c) of The cardinality of a finite set.
Definition. For (The natural numbers (von Neumann)) set
the derangement number. Since , the previous paragraph gives for every finite set .
Three values, read off the definition and not stipulated.
- . Here , the only function is the empty function, it is a bijection, and the condition " for every " holds vacuously. So .
- . Here and the only bijection of is the identity, which fixes .
- . Here , the two bijections are the identity and the exchange of and , and only the second is fixed-point free.
Remarks
-
A set of bijections, with no group vocabulary. The object counted is a set of functions. Nothing among this page's declared prerequisites defines a symmetric group, a permutation cycle or a conjugacy class, and no result about stated here needs one.
-
is not a convention. It is what the definition returns at , and it is the value that makes the closed formula and the first recurrence true at their first legal index. A text that sets "by convention" is stipulating what is here computed.
, with the term at equal to and
Statement
For every , in ,
where is the derangement number (The derangement number : the number of bijections of an -element set with no fixed point), the factorial (The factorial and the falling factorial , defined by recursion in ) and the canonical natural (The canonical natural of a field). Each division is legitimate because , hence .
The index runs from , and the term at is . At the identity reads , which agrees with ; at it reads ; and at it reads .
Since is injective, the identity determines as a natural number (Laws of finite sums and products in , and , clause 7).
Facts & Assumptions
Given: A natural number , the set of bijections of onto itself, and, for , the set of bijections fixing .
is finite with for every finite (A finite set with has exactly bijections onto itself, and bijections onto any set of the same cardinality, The factorial and the falling factorial , defined by recursion in ); in particular and (The cardinality of a finite set).
is a family of subsets of the finite set indexed by the finite set , hence a sieve family with ambient set , and (A finite family of subsets of a finite set , the intersections for , and the convention , A subset of a finite set is finite, with , and equality holds if and only if ).
, since a bijection of is a derangement exactly when it fixes no point (The derangement number : the number of bijections of an -element set with no fixed point, Injection, surjection, bijection).
For a finite sieve family in with , the complementary identity is (Inclusion and exclusion: , together with the complementary form counting the elements in none of the , clause 2).
Partition of a power set by cardinality: the sets for are pairwise disjoint with union , and (A subset of a finite set is finite, with , and equality holds if and only if , clause 2, The set of -element subsets and the binomial coefficient , for finite ).
Splitting a sum along a partition of its index set (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 3); a constant real summand and the bridge (The sum over a finite index set, and its product form, clauses (a) and (c)); and scaling of a real finite sum (Laws of finite sums and finite products, clause 2, Finite sums and finite products, by recursion).
For : , so with the truncated difference (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 1, Finite sums and finite products of natural numbers, and in ).
Integrality of the binomial coefficient: for , ( for ; hence , the quotient is a natural number, and , clause 2); and for every , so (The factorial and the falling factorial , defined by recursion in , clause (b), Laws of finite sums and products in , and , clause 7).
is an ordered field, so division by a nonzero element is available (Ordered field, Field); and (Integer powers ).
Proof
The ambient set and the sieve family. is finite with by [L1], the sets for are subsets of , and is the complement in of their union by [L3].
The intersections are bijection sets of a smaller set. For the map is a bijection of onto . Indeed a bijection of fixing every point of has , hence by injectivity, so its restriction is a bijection of ; conversely a bijection of extends by the identity on to a bijection of fixing every point of , and the two constructions are mutually inverse. For both sides are , by the stipulation of [L2].
Hence for every , by [L1] applied to and by [L7].
The sieve. Applying [L4] to the family of step 1.1 and substituting step 1.3, .
Grouping the subsets of by size. Splitting along the partition of [L5] and using the constant clause of [L6] on each block, where the summand depends on only through , gives .
Each coefficient collapses. For , that is , [L8] gives , so the -th summand of step 3.1 is ; scaling the sum by the constant through [L6] gives .
Remarks
-
Where the closed formula for the binomial coefficient is spent. Only in the last step, and only in the range , which is exactly the range the sum runs over. Outside that range the identity of for ; hence , the quotient is a natural number, and is not asserted, and it is not used.
-
Why the identity is stated in . It contains both a subtraction, through the alternating sign, and a division by . Neither operation exists in , so the count is carried across by ; injectivity of is what carries the conclusion back.
-
The first index is and it matters. The term at is , and the identity at is the statement , which is where the empty function enters. A version of this formula whose sum began at would be false at every .
for , and for
Statement
Let be the derangement numbers (The derangement number : the number of bijections of an -element set with no fixed point) and the canonical natural (The canonical natural of a field). Then:
- For every , in ,
- For every , in ,
All differences are the truncated ones (Finite sums and finite products of natural numbers, and in ), which in the stated ranges are the ordinary ones.
Both hypotheses are exactly what the proofs need, and nothing is asserted outside them. Clause 1 is proved from the identity and its consequence , both of which fail at under the truncated difference, where is ; so is its first legal index, and there it reads . Clause 2 is derived by applying clause 1 twice, at and at , so it needs ; its first legal index is , where it reads . Under the truncated difference the two displayed formulas happen also to be true at and at respectively, both sides being in the first case and in the second, but neither of those readings is proved here and neither is claimed.
Facts & Assumptions
Given: A natural number with in clause 1 and in clause 2; the abbreviation , so that (Order on the natural numbers, Finite sums and finite products of natural numbers, and in , Every nonzero natural number is a successor).
The derangement formula: for every (, with the term at equal to and ).
Recursion clause of the real finite sum: (Finite sums and finite products, by recursion, Laws of finite sums and finite products).
Factorials: , so when ; and for every (The factorial and the falling factorial , defined by recursion in ).
is additive and multiplicative with , and it is injective (Laws of finite sums and products in , and , clauses 0 and 7, The canonical natural of a field). In particular when , and .
Powers of : and (Integer powers ).
is an ordered field, so subtraction and division by a nonzero element are available (Ordered field, Field).
Proof
Let and put , so . Then by [L3], hence by [L4], and both and are nonzero.
The formula at . By [L1] and , .
Splitting the sum at its last index. By [L2], .
Clause 1. Multiplying step 1.3 by and using [L1] at , step 1.1 and step 1.2, .
Now let , so that and . Applying step 2.1 at in place of gives , hence ; and by [L5], so .
Clause 2. Substituting step 3.1 into step 2.1, , using from [L4]; the right-hand side is by the additivity and multiplicativity of , so by injectivity.
Remarks
-
Clause 2 is derived from clause 1 and not from the formula. Two instances of clause 1, at and at , are enough, and that is why clause 2 begins one index later: the second instance needs .
-
Why clause 1 is stated in and clause 2 in . Clause 1 carries the term , which is not a natural number when is odd. Clause 2 has no signs left in it, both sides are counts, and injectivity of carries the identity back into where it belongs.
-
The truncated difference is why the hypotheses have to be written out. Under it the symbols and never become ill formed: at the first reads and at the second reads as well. So a reader cannot tell from the shape of the formula where it stops being proved, and the ranges and have to be stated rather than inferred.
A finite list of reals, and its strictly increasing and strictly decreasing sublists
Definition
Let (The natural numbers (von Neumann)). A finite list of reals of length is a function , written for ; here is the von Neumann natural itself (On the order is membership: , Order on the natural numbers), so the indices are and the list of length is the empty function. The list is pairwise distinct when is injective, that is when whenever (Injection, surjection, bijection).
A sublist of of length , for , is a function that is strictly increasing on indices, meaning whenever ; its terms are . Such an is injective, since natural-order trichotomy gives or when , and hence (Trichotomy of the order on ).
The sublist is
- strictly increasing when for all ;
- strictly decreasing when for all ,
the order being that of the ordered field (Ordered field).
Boundary readings, which are part of the definition and not exceptions. A sublist of length or has no pair at all, so it is both strictly increasing and strictly decreasing, vacuously. A list of length has a sublist of length exactly when , namely for any ; and it has no sublist of length with , since would be an injection of into , contrary to the finite pigeonhole principle (The pigeonhole principle on , clause 2).
Every count here is a natural number. The length of a list and the length of a sublist are naturals, and no cardinality of an infinite set is used; a list is a function on a natural number, so it is finite in the sense of The cardinality of a finite set.
Remarks
-
A sublist is a choice of positions, not a choice of values. Two positions carrying equal values are different sublists of length . This is why the monotonicity conditions are stated on and rather than on a set of values, and why the pairwise-distinctness hypothesis has to be imposed separately when a result needs it.
-
Strictness on both sides. The indices increase strictly, so a sublist reads the list left to right without repeating a position; the values increase or decrease strictly, so no two terms of a monotone sublist are equal. Neither strictness is redundant: a list may repeat a value, and then a nondecreasing sublist could be longer than any strictly increasing one.
-
The empty list. At the only sublists are the empty one, of length . Any statement asserting the existence of a sublist of length is therefore false at , and any statement about lists of length has content at or precisely because .
Every list of pairwise distinct reals has a strictly increasing sublist of length or a strictly decreasing sublist of length
Statement
Let and let be a pairwise distinct finite list of reals of length (A finite list of reals, and its strictly increasing and strictly decreasing sublists). Then has a strictly increasing sublist of length or a strictly decreasing sublist of length .
The length is at least for all and , so the statement has content at every pair of indices. At the list has one term and the required increasing sublist has length , which the single position supplies; at the same reading holds for the decreasing sublist, and the increasing one of length is also available.
Facts & Assumptions
Given: Naturals and , the length , and a pairwise distinct list . For and , call an increasing run ending at when is a strictly increasing sublist of (in both senses of A finite list of reals, and its strictly increasing and strictly decreasing sublists) with , and define a decreasing run ending at in the same way with the values strictly decreasing.
A nonempty subset of with an upper bound has a greatest element. Let be nonempty with for some . Every then satisfies by On the order is membership: , so the set contains and has a least element by The well-ordering principle. If then every satisfies and , hence and by Discreteness: is the immediate successor; since is nonempty, , so for some (Every nonzero natural number is a successor) and for every , putting below and contradicting minimality. So and is the greatest element of .
For every there is an increasing run and a decreasing run ending at , both of length : take with , which is vacuously monotone in both senses (A finite list of reals, and its strictly increasing and strictly decreasing sublists).
Every run has length at most : a run of length is injective into , and there is no injection of into when (The pigeonhole principle on , clause 2, Injection, surjection, bijection, A finite list of reals, and its strictly increasing and strictly decreasing sublists).
Order facts in : , and (On the order is membership: , Order on the natural numbers, The natural numbers (von Neumann)); exactly one of , , holds (Trichotomy of the order on ); (Discreteness: is the immediate successor); every nonzero natural is a successor (Every nonzero natural number is a successor); and the truncated difference of Finite sums and finite products of natural numbers, and in , for which gives .
and (The product rule: , and , clause 1, The cardinality of a finite set); and there is no injection for any (The pigeonhole principle on , clause 1). A bijection exists because the two sets have the same cardinality (The cardinality of a finite set, clause (d)).
is an ordered field, so its order is total and gives or (Ordered field, Field).
Proof
If or , then , and the one-term sublist ending at supplied by [L2] has the required length or , respectively. Hence assume and suppose, for contradiction, that has neither required sublist.
The two run lengths. For let be the set of lengths of increasing runs ending at and the set of lengths of decreasing runs ending at . Both are nonempty by [L2] and both are contained in by [L3] and [L4], so both have a greatest element by [L1]; write and for those greatest elements. Both are at least .
The bound imposed by the supposition. If some were at least , truncating a longest increasing run ending at to its first positions would give a strictly increasing sublist of length ; so for every by [L4], and likewise . Combined with and from step 1.2, this gives and , so the map sends into .
Extending a run. Let . If and is an increasing run of length ending at , then defined by and is again a strictly increasing sublist: its indices increase because , and its values increase because for . So and . Symmetrically, if then .
is injective. Let ; since is pairwise distinct, , so or by [L6]. In the first case step 2.2 gives , in the second ; either way , because both run lengths are at least , so by [L4] and equal first coordinates would force equal run lengths, and likewise for the second coordinate. As and were an arbitrary pair of distinct indices, is injective.
The contradiction. Composing with a bijection from [L5] gives an injection of into , which [L5] forbids. So the supposition of step 1.1 is untenable, and has a strictly increasing sublist of length or a strictly decreasing sublist of length .
Remarks
-
Where pairwise distinctness is spent. Only in step 3.1, to force one of the two strict comparisons between and . Without it a list may repeat a value, and then two positions carrying that value force neither run length to increase.
-
Why a greatest element exists at all. The lengths of runs ending at a fixed position form a nonempty set of naturals bounded by the length of the list, and a nonempty bounded set of naturals has a greatest element; that is derived in the facts from the well-ordering principle alone. No maximum of a finite set of reals is involved, and no choice principle is used, since and are determined by rather than selected.
-
The bound is not improvable, and the witness is a list of distinct reals with neither long sublist; it is constructed in For all and there is a list of pairwise distinct reals with no strictly increasing sublist of length and no strictly decreasing sublist of length .
For all and there is a list of pairwise distinct reals with no strictly increasing sublist of length and no strictly decreasing sublist of length
Statement
Let . Then there is a pairwise distinct finite list of reals (A finite list of reals, and its strictly increasing and strictly decreasing sublists) with no strictly increasing sublist of length and no strictly decreasing sublist of length .
Together with the bound , this says that is the least length at which the two alternatives become unavoidable.
At or the list is empty, and there is no sublist of any positive length at all, so the assertion holds for the trivial reason that both required sublists have length at least .
Facts & Assumptions
Given: Naturals and , the finite sets and , and the ordered field with the canonical natural (The canonical natural of a field).
Arithmetic and order of : addition and multiplication are as in Addition of natural numbers and Multiplication of natural numbers; means for a unique , written (Order on the natural numbers, Addition is cancellative, Finite sums and finite products of natural numbers, and in ), and is transitive ( is a linear order on ); if and only if (Discreteness: is the immediate successor); (Order is compatible with addition); addition is commutative (Addition is commutative); (Distributivity and the successor law for multiplication); multiplication is monotone in its first factor, since gives by commutativity and distributivity (Multiplication is commutative, Distributivity and the successor law for multiplication), so implies ; exactly one of , , holds (Trichotomy of the order on ); and (On the order is membership: ).
and for a natural (The product rule: , and , clause 1, The cardinality of a finite set).
An injection between finite sets of equal cardinality is a bijection: it is a bijection onto its image, the image has the same cardinality as the domain, and clause 3 of A subset of a finite set is finite, with , and equality holds if and only if then makes the image the whole codomain (The cardinality of a finite set, Injection, surjection, bijection).
There is no injection of into when (The pigeonhole principle on , clause 2).
is strictly increasing, hence injective (Laws of finite sums and products in , and , clause 7); and is an ordered field (Ordered field, Field).
Sublists (A finite list of reals, and its strictly increasing and strictly decreasing sublists): a sublist of length is a strictly increasing , hence injective; it is strictly increasing, respectively decreasing, when its values do the same.
Proof
If or , then and the empty list has no sublist of the positive lengths and , proving the assertion in these boundary cases. Hence for the construction below assume .
The index bijection. Define by . Its values lie in : from and we get and , so by [L1], whence .
is injective. Suppose with . If then , so by [L1], a contradiction; symmetrically is impossible, so by [L1], and then by cancellation.
The list. By [L2] and [L3], the injection of step 1.3 is a bijection of onto , so every index is for exactly one pair, and defines a list . Write for the block of an index.
Inside a block the values decrease. Let and . Then by [L1], while and with , so and hence by [L1] and [L5].
Across blocks the values increase, and the block is monotone in the index. Let and . Then , the last step because ; so by [L5]. Moreover , by the computation of step 1.3; equivalently, is nondecreasing along the index order.
The list is pairwise distinct. Two indices with different blocks carry different values by step 3.2, and two indices in the same block carry different values by step 3.1; since every index has exactly one block by step 2.1, distinct indices carry distinct values.
No strictly increasing sublist of length . Let be a strictly increasing sublist. The map is injective: if had , then lie in one block, so by step 3.1, contradicting that the sublist increases. Hence by [L4] and natural-order trichotomy, so .
No strictly decreasing sublist of length . Let be a strictly decreasing sublist and let . Then , so by step 3.2; and would give by step 3.2, contradicting that the sublist decreases. Thus, if , all the lie in the block of , say , and is injective into because is injective and is a bijection. If , the empty map is already an injection . In either case [L4] and natural-order trichotomy give , so .
Together with the boundary cases in step 1.1, the list of step 2.1 is therefore a pairwise distinct list of reals with no strictly increasing sublist of length and no strictly decreasing sublist of length , which is the assertion.
Remarks
-
The two block counts are not interchangeable. The construction uses blocks of terms each. An increasing sublist meets each block at most once, so its length is bounded by the number of blocks, ; a decreasing sublist lies inside one block, so its length is bounded by the block size, . Exchanging the roles would bound the increasing sublists by and the decreasing ones by , which is the sharpness statement for the pair and not for .
-
Why the values are written through . The terms of a list of reals are real numbers, and is a natural number, which is a set and not an element of . The strict monotonicity of is what transports the comparisons between the naturals into comparisons between the terms.
-
The degenerate cases are discharged first. If or then and are both empty, and step 1.1 proves directly that the empty list has neither required positive-length sublist.
The conventions this page fixes: the empty intersection, where the counts live, the first index of every sum, and what the declared prerequisites do not supply
This item is the page's ledger: every convention the page fixes, with the item
that fixes it, and a statement of what this page's declared prerequisites do not
supply. It continues Conventions fixed on this page, and what counting is deliberately not done here, the same kind of
ledger for the page finite-counting-and-binomial-coefficients, which is this
page's declared prerequisite.
Conventions fixed here
The empty intersection is the ambient set, and the ambient set is part of the data. A finite family of subsets of a finite set , the intersections for , and the convention fixes a finite together with the family and stipulates . This is a stipulation and not a theorem: for nonempty the intersection is determined by the family, and for the description "belongs to every with " is satisfied by everything, so it determines nothing without an ambient set to be relative to. The clause supplies the term in the complementary form of Inclusion and exclusion: , together with the complementary form counting the elements in none of the and in later sieves whenever an intersection must also be identified at the empty subfamily.
Counts live in ; every alternating identity lives in . A cardinality is a natural number, a natural number here is a set, and a set is not an element of . Every identity on this page that uses a negative summand, and every one that divides counts, is therefore stated in with the counts carried across by the canonical natural (The canonical natural of a field), and read back through the injectivity of where the conclusion is about natural numbers. Truncated natural differences such as and remain in and are not negative summands.
Every index range starts at , and the lower-bound hypotheses on this page exist only because of it. for every and every carries ; without it the identity fails at and . for , and for carries in its first clause, because the identity that proves it fails at under the truncated difference, and in its second, because that clause applies the first one at . for naturals and : the least with carries , without which the set it takes a least element of can be empty.
, and the place it is spent is named. The convention is the base clause of the recursion in Exponentiation of natural numbers, , and its agreement with the integer power in , not an import. In The number of surjections from an -element set onto a -element set is , read in through it is what makes the formula correct at and , where the empty function is the unique surjection and the formula returns . At with the same formula returns the full alternating row sum, which vanishes only because ; and at with it returns , which is for the same reason read the other way. Powers of are the real powers of Integer powers throughout, since is not a natural number.
A sum over a finite index set is what all of this is written in. The sum over a finite index set, and its product form is the notion used for every sum whose index set is a set of subsets, a set of elements or a relation's fibre family, and its value is independent of the enumeration chosen. The facts about it that are used constantly and are not clauses of it are the bridge over such an index set, and the additivity, scaling and monotonicity laws over such an index set. Both are derived, in the Facts of the items that use them, from the corresponding clauses about a sum over an initial segment together with the enumeration that defines the sum over an index set.
A relation, not a matrix. A relation between finite sets, its row fibres and its column fibres sets up a subset of a product of two finite sets, its two fibre families and their slice partitions. Double counting: for a relation between finite sets states the resulting equality of the two fibre sums with the size of the relation, and nothing more.
Fibres of a function. If then every has a fibre with more than elements, and for nonempty some fibre has at least elements is stated about the fibres of a function between finite sets. Its two clauses are one argument: the ceiling form is the counting form applied at the single index below the ceiling, which is why the ceiling was defined by minimality.
What this page's declared prerequisites do not supply
Each of the following is a statement about what this page may cite, and about nothing else.
-
No floor and no ceiling as general notions, and no division with remainder. for naturals and : the least with defines only the least with , for naturals and . It is not defined for a real argument, it produces no remainder, and nothing here extends it.
-
No divisibility. No result on this page is stated in terms of one natural number dividing another, and no argument uses such a relation.
-
No graph vocabulary. Nothing among this page's declared prerequisites defines a graph, a vertex or an edge. The results that would usually be stated about graphs are stated instead about a finite set carrying a symmetric irreflexive relation, which is exactly what their proofs use.
-
No probability. Nothing among this page's declared prerequisites defines a probability space, a measure or an expectation. The averaging principle is a statement about a quotient of two counts, and the hat-check ratio on the companion page is a quotient of two counts; neither is called a probability and neither is treated as one.
-
No symmetric group. The derangement number : the number of bijections of an -element set with no fixed point counts a set of bijections. No group structure on that set is defined or used.
5 · Examples, counterexamples and false statements
FALSE: the real-valued three-set inclusion-exclusion identity remains true after deleting the triple-intersection term
Statement
FALSE. The statement
for all finite sets , , , in ,
This is the sieve identity of Inclusion and exclusion: , together with the complementary form counting the elements in none of the for a family of three sets with the term at the triple intersection deleted. The identity is correct only when the triple term is present, and the claim above is refuted by a family in which that term is not .
Facts & Assumptions
Given: The one-element set , taken inside the ambient set , and the canonical natural (The canonical natural of a field).
and (The cardinality of a finite set, clause (a), The canonical natural of a field).
The sieve identity for a finite family of subsets of a finite ambient set, in the form (Inclusion and exclusion: , together with the complementary form counting the elements in none of the , clause 1, A finite family of subsets of a finite set , the intersections for , and the convention , The sum over a finite index set, and its product form).
and , so , and (Integer powers ).
is an ordered field, so and its arithmetic is available (Ordered field, Field).
Refutation
Take , and , so that the family of the displayed claim is , , . Every intersection of a nonempty subfamily is , and the union is .
Every set occurring in the computation is , so by [L1] each of , , , , , , and equals .
The right-hand side of the displayed claim is therefore , while its left-hand side is . Since in by [L4], the claim is false at this family.
The true identity at the same family. By [L2] the sieve sum has the three singleton terms with sign , the three two-element terms with sign and the one three-element term with sign , so it reads , which is . The deleted triple term is exactly the discrepancy found in step 2.1.
Remarks
-
The claim is the sieve truncated at depth , and the Bonferroni inequalities say what such a truncation does in general: an even truncation under-estimates. Here it under-estimates by , and the claim asserts equality, so the failure is in the direction the inequality predicts.
-
The witness is as small as it can be. Three sets are needed for a triple intersection to exist, and the discrepancy is the size of that intersection, so any family with a nonempty triple intersection refutes the claim. Taking all three sets equal to a single point makes every cardinality in the computation equal to .
FALSE: truncating the sieve at a fixed depth of at least two gives the exact size of the union
Statement
FALSE. The statement
for every sieve family , , and every ,
with and as in Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it.
The claim reads the Bonferroni inequalities as if a truncation at any depth beyond the first were already exact. What is true is that the truncation is an over-estimate at an odd depth and an under-estimate at an even depth, and that it is guaranteed to become exact once the depth reaches , though special families may become exact earlier; the hypothesis does nothing to close that gap when exceeds .
Facts & Assumptions
Given: The ambient set , the index set , the family , and the truncation depth .
and ; a constant real summand gives (Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it, The sum over a finite index set, and its product form, clause (c), Finite sums and finite products, by recursion, Laws of finite sums and finite products).
and (Integer powers ); is an ordered field, so (Ordered field, Field).
Refutation
The witness. With and , every with is , and the union is , so by [L1].
The first two truncation levels. Each summand is by step 1.1, so and by [L2] and the constant clause of [L3]; likewise .
Therefore , while . Since by [L4], the displayed claim fails at this family and at , which satisfies its hypothesis .
What is true here instead. Clause 2 of Truncating the sieve at an odd depth over-estimates the size of the union and truncating it at an even depth under-estimates it gives , and indeed ; and , which is the exact value, in agreement with clause 3 of that theorem at . So the truncation becomes exact one level later than the claim asserts, and the gap at depth is the whole content of the failure.
Remarks
-
The claim is not repaired by raising the fixed depth. For any fixed the same all-equal family with taken to have more than elements refutes it again; clause 3 guarantees exactness once the depth reaches , while other families may already be exact sooner. That is why the true uniform guarantee fixes the depth relative to rather than absolutely.
-
The direction of the error is not accidental. Depth is an even truncation, and an even truncation under-estimates, so the truncated value is below the truth rather than above it. A witness at depth would over-shoot instead.
FALSE: every list of pairwise distinct reals has a strictly increasing sublist of length or a strictly decreasing sublist of length
Statement
FALSE. The statement
for all , every pairwise distinct finite list of reals of length has a strictly increasing sublist of length or a strictly decreasing sublist of length (A finite list of reals, and its strictly increasing and strictly decreasing sublists).
This is Every list of pairwise distinct reals has a strictly increasing sublist of length or a strictly decreasing sublist of length with the length lowered from to . The true theorem is sharp, so lowering the length by one destroys it, and it does so at every pair rather than at some exceptional pair.
Facts & Assumptions
Given: The naturals and , and lists of reals with their sublists as in A finite list of reals, and its strictly increasing and strictly decreasing sublists.
For all there is a pairwise distinct list of reals of length with no strictly increasing sublist of length and no strictly decreasing sublist of length (For all and there is a list of pairwise distinct reals with no strictly increasing sublist of length and no strictly decreasing sublist of length ).
Every pairwise distinct list of reals of length has a strictly increasing sublist of length or a strictly decreasing sublist of length (Every list of pairwise distinct reals has a strictly increasing sublist of length or a strictly decreasing sublist of length ).
(Multiplication of natural numbers, Order on the natural numbers), and the terms of a list are elements of the ordered field (Ordered field).
Refutation
Read the displayed claim at : every pairwise distinct list of reals of length would have a strictly increasing sublist of length or a strictly decreasing sublist of length .
By [L1] at there is a pairwise distinct list of reals of length with no strictly increasing sublist of length and no strictly decreasing sublist of length .
That list refutes the reading of step 1.1, so the displayed claim is false. The same argument runs at every pair , since [L1] produces a witness for each of them; the claim therefore fails everywhere, not at an exceptional pair.
What survives is [L2]: the conclusion holds once the length is raised to . So the least length at which the alternative becomes unavoidable is , and the claim above is exactly the assertion that it is .
Remarks
-
The false statement is not weaker in one place and true in another. The witness of For all and there is a list of pairwise distinct reals with no strictly increasing sublist of length and no strictly decreasing sublist of length exists for every pair of naturals, so there is no range of and in which the lowered bound holds.
-
The degenerate pairs fail too, and for a different reason. At or the length is , the list is empty, and it has no sublist of any positive length; both alternatives ask for a sublist of length at least . At those pairs the claim fails without any construction being needed.
Sources
Standard references
Recommended treatments; not extraction sources.
- Summation (Wikipedia)
- Double counting (proof technique) (Wikipedia)
- R. Stanley, Enumerative Combinatorics, Vol. 1, Ch. 1
- Mathematics for Computer Science (MIT OpenCourseWare)
- Pigeonhole principle (Wikipedia)
- Floor and ceiling functions (Wikipedia)
- Well-ordering principle (Wikipedia)
- Sylvestre, Pigeonhole Principle (LibreTexts)
- Inclusion-exclusion principle (Wikipedia)
- R. Stanley, Enumerative Combinatorics, Vol. 1, Ch. 2
- Guichard, The Inclusion-Exclusion Formula (LibreTexts)
- Binomial coefficient (Wikipedia)
- Pascal's rule (Wikipedia)
- Indicator Functions and Inclusion-Exclusion (University of South Carolina notes)
- Boole's inequality (Wikipedia)
- Principle of Inclusion and Exclusion and Bonferroni Inequalities (Concordia notes)
- Surjective function (Wikipedia)
- Twelvefold way (Wikipedia)
- Algebraic Combinatorics Blueprint: Surjections
- Derangement (Wikipedia)
- Rencontres numbers (Wikipedia)
- DLMF §26.13: Permutations: Cycle Notation
- Derangements (OpenText at the University of Lethbridge)
- Principle of Inclusion and Exclusion (Open Math Books)
- Erdos-Szekeres theorem (Wikipedia)
- Longest increasing subsequence (Wikipedia)
- Morris, Combinatorics: The Pigeonhole Principle (LibreTexts)
- Cardinality (Wikipedia)