LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-07-31

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 Boolean lattice on an $n$ -element set has $n!$ maximal chains, and exactly $k!(n-k)!$ contain a fixed $k$ -set

Statement

Let $A$ be an $n$ -element set. The Boolean lattice $B(A)$ has exactly $n!$ maximal chains. If $S\subseteq A$ has cardinality $k$ , then exactly $k!(n-k)!$ maximal chains contain $S$ .

Facts & Assumptions

Given: A finite set $A$ with $|A|=n$ and a subset $S\subseteq A$ with $|S|=k$ .

[F1]

The Boolean lattice is $\mathcal P(A)$ ordered by inclusion, with rank $|T|$ ; a chain is a pairwise comparable subset, and a maximal chain is a chain contained in no larger chain (The Boolean lattice of subsets of a finite set and its rank levels, Chain in a poset).

[L1]

A finite $m$ -element set has exactly $m!$ bijections from any other $m$ -element set (A finite set $A$ with $\lvert A\rvert = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality, The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $\mathbb{N}$ ).

[L2]

Independent finite choices multiply their cardinalities (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$ ).

[L3]

For $k\le n$ , $\binom nk\,k!(n-k)!=n!$ ( $\binom{n}{k}\,k!\,(n-k)! = n!$ for $k \le n$ ; hence $\binom{n}{k}\,k! = n^{\underline{k}}$ , the quotient $n!/(k!(n-k)!)$ is a natural number, and $\binom{n}{k} = \binom{n}{n-k}$ ).

Proof

technique · direct

1.1

Every ordering $(a_1,\ldots,a_n)$ of $A$ determines the maximal chain $\varnothing\subset\{a_1\}\subset\{a_1,a_2\}\subset\cdots\subset A$ .

givenF1construct

2.1

Conversely, a maximal chain contains exactly one set of each rank from $0$ to $n$ , and the unique element added between consecutive ranks recovers an ordering of $A$ . Thus the correspondence in step 1.1 is bijective.

step 1.1F1

2.2

A chain from an ordering contains $S$ exactly when its first $k$ entries are the elements of $S$ . There are $k!$ orders for those entries and $(n-k)!$ orders for the remaining entries, independently.

step 1.1L1

3.1

By [L1], there are $n!$ orderings of $A$ , so steps 1.1 and 2.1 give exactly $n!$ maximal chains.

step 1.1step 2.1L1

4.1

The product rule therefore gives exactly $k!(n-k)!$ maximal chains through $S$ . Summing this count over the $\binom nk$ possible $S$ agrees with the total $n!$ by [L3].

step 3.1step 2.2L2L3∎

Depends on

Used by

Lubell-Yamamoto-Meshalkin inequality for antichains in a Boolean lattice Theorem

Dependency tree · next 3 levels

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

M. Keller and W. T. Trotter, Applied Combinatorics, §6.2 (standard reference, not scraped)

The Boolean lattice on an nnn-element set has n!n!n! maximal chains, and exactly k!(n−k)!k!(n-k)!k!(n−k)! contain a fixed kkk-set