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

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\le a\text{ for some }a\in A\},\qquad P^+:=\{x\in P:a\le x\text{ 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\setminus 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\le x\le a$ , hence $b\le a$ by transitivity. Since $A$ is an antichain, $a=b$ , and antisymmetry applied to $a\le x\le a$ gives $x=a\in A$ .

givenF1F2

2.1

For the comparable pair from step 1.1, either $x\le a$ and $x\in P^-$ , or $a\le 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\le 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 27 results over 11 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.4 (standard reference, not scraped)