LemmaStatement: AI-adaptedProof: 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.

A maximal antichain splits a finite poset into its down-set and up-set with the antichain as their intersection

Statement

Let $P$ be a finite poset and let $A$ be a maximal antichain. Define

$P^{-} : = {x \in P : x \leq a for some a \in A}, P^{+} : = {x \in P : a \leq x for some a \in A} .$

Then $P = P^{-} \cup P^{+}$ and $P^{-} \cap P^{+} = A$ . Both sets carry the order induced from $P$ .

Facts & Assumptions

Given: A finite poset $P$ , a maximal antichain $A \subseteq P$ , and the subsets $P^{-}$ and $P^{+}$ in the Statement.

[F1]

An antichain has pairwise incomparable distinct elements and is maximal when no strictly larger antichain contains it (Antichains, chain covers, and antichain covers of a poset).

[F2]

A partial order is reflexive, antisymmetric, and transitive (Partial order and partially ordered set).

Proof

technique · direct

1.1

If $x \in P ∖ A$ were incomparable with every $a \in A$ , then $A \cup {x}$ would be a larger antichain. Maximality therefore gives an $a \in A$ comparable with $x$ .

givenF1

1.2

Let $x \in P^{-} \cap P^{+}$ . There are $a, b \in A$ with $b \leq x \leq a$ , hence $b \leq a$ by transitivity. Since $A$ is an antichain, $a = b$ , and antisymmetry applied to $a \leq x \leq a$ gives $x = a \in A$ .

givenF1F2

2.1

For the comparable pair from step 1.1, either $x \leq a$ and $x \in P^{-}$ , or $a \leq x$ and $x \in P^{+}$ . Every member of $A$ lies in both sets by reflexivity, so $P = P^{-} \cup P^{+}$ .

step 1.1F2

2.2

Conversely, every $a \in A$ satisfies $a \leq a$ , so $A \subseteq P^{-} \cap P^{+}$ . Together with step 1.2 this gives $P^{-} \cap P^{+} = A$ .

step 1.2F2

3.1

Steps 2.1 and 2.2 establish the asserted union and intersection; restricting the order of $P$ to either subset again gives a partial order.

step 2.1step 2.2F2∎

Depends on

Used by

The down-set and up-set chain covers from a suitable maximum antichain splice to a width-sized chain cover Lemma

Dependency tree · two levels

11 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

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