CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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 complementary inclusion-exclusion formula is Möbius inversion on the Boolean lattice

Statement

For a finite sieve family $(A_{i})_{i \in I}$ in a finite ambient set $X$ , let $ι : N \to R$ be the canonical natural map used in Inclusion and exclusion: $ι ∣ ⋃_{i \in I} A_{i} ∣ = \sum_{\emptyset \neq J \subseteq I} (- 1)^{∣ J ∣ + 1} ι ∣ A_{J} ∣$ , together with the complementary form counting the elements in none of the $A_{i}$ . The complementary inclusion-exclusion identity

$ι ∣ X ∖ ⋃_{i \in I} A_{i} ∣ = \sum_{J \subseteq I} (- 1)^{∣ J ∣} ι ∣ A_{J} ∣$

in $R$ is exactly the upper-finite Möbius inversion formula on the Boolean lattice $P (I)$ .

Facts & Assumptions

Given: A sieve family $X, I, (A_{i})_{i \in I}$ , its intersections $A_{J}$ , and the trace $T (x) : = {i \in I : x \in A_{i}}$ (A finite family $(A_{i})_{i \in I}$ of subsets of a finite set $X$ , the intersections $A_{J}$ for $J \subseteq I$ , and the convention $A_{\emptyset} = X$ ).

[F1]

For $J \subseteq I$ , $x \in A_{J}$ exactly when $J \subseteq T (x)$ , including $A_{\emptyset} = X$ ; and $x \notin ⋃_{i} A_{i}$ exactly when $T (x) = \emptyset$ (A finite family $(A_{i})_{i \in I}$ of subsets of a finite set $X$ , the intersections $A_{J}$ for $J \subseteq I$ , and the convention $A_{\emptyset} = X$ ).

[L1]

Both forms of Möbius inversion hold on the finite Boolean lattice (Both forms of Möbius inversion hold on every finite poset).

[L2]

Its Möbius function is $μ (J, K) = (- 1)^{∣ K ∖ J ∣}$ (For $A \subseteq B$ in a finite Boolean lattice, $μ (A, B) = (- 1)^{∣ B ∖ A ∣}$ ).

[L3]

The complementary inclusion-exclusion theorem uses the canonical map $ι : N \to R$ , has the displayed terms, and adopts the convention $A_{\emptyset} = X$ (Inclusion and exclusion: $ι ∣ ⋃_{i \in I} A_{i} ∣ = \sum_{\emptyset \neq J \subseteq I} (- 1)^{∣ J ∣ + 1} ι ∣ A_{J} ∣$ , together with the complementary form counting the elements in none of the $A_{i}$ ).

Proof

technique · direct

1.1

For $K \subseteq I$ , let $h (K) : = ι ∣ {x \in X : T (x) = K} ∣$ , and let $g (J) : = ι ∣ A_{J} ∣$ . The trace classes partition $A_{J}$ , and [F1] gives $g (J) = \sum_{K \supseteq J} h (K)$ in $R$ .

F1L3

2.1

Apply the upper-finite form of [L1] at $J = \emptyset$ : $h (\emptyset) = \sum_{K \supseteq \emptyset} μ (\emptyset, K) g (K)$ .

step 1.1L1

3.1

By [F1], $h (\emptyset) = ι ∣ X ∖ ⋃_{i} A_{i} ∣$ , and by [L2], $μ (\emptyset, K) = (- 1)^{∣ K ∣}$ . Substitution in step 2.1 gives $ι ∣ X ∖ ⋃_{i} A_{i} ∣ = \sum_{K \subseteq I} (- 1)^{∣ K ∣} ι ∣ A_{K} ∣$ .

step 2.1F1L2

4.1

The identity in step 3.1 matches [L3] term for term, including the empty-subset term $ι ∣ A_{\emptyset} ∣ = ι ∣ X ∣$ ; hence complementary inclusion-exclusion is Boolean-lattice Möbius inversion.

step 3.1L3∎

Depends on

Used by

False: classical Möbius inversion and inclusion-exclusion are unrelated inversion principles False statement

Dependency tree · two levels

27 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

R. Stanley, Enumerative Combinatorics, Volume 1, §§3.6–3.8 (standard reference, not scraped)