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 anticonnected components of are exactly the connected components of
Statement
For every graph , its anticomponents are exactly the vertex sets of the connected components of . In particular, they partition .
Facts & Assumptions
Given: A finite graph .
Anticomponents are defined to be the component vertex sets of (Anticonnected graphs and anticonnected components).
Connected components partition a graph's vertex set (The connected components of a graph partition its vertex set and are its maximal connected subgraphs).
( for every vertex set ).
Proof
By F1, a set is an anticomponent of exactly when it is the vertex set of a connected component of .
Equivalently, is connected and is maximal with this property.
The component partition theorem applied to shows that these sets partition .
Depends on
Used by
- Every P₄-free graph has a clique or stable set of size at least the square root of its order Corollary
- Distinct connected components are anticomplete, and distinct anticonnected components are complete Lemma
- Every union of connected components is a module, and so is every union of anticonnected components Lemma
- A pure blockade with a cograph pattern has additive kappa Theorem
- Every prime graph on at least four vertices contains an induced P₄ Theorem
- Gallai's modular decomposition theorem: a graph on at least two vertices is disconnected, or has a disconnected complement, or has a modular partition into its maximal proper modules whose quotient is prime Theorem
- The cographs are exactly the P₄-free graphs Theorem
Dependency tree · two levels
7 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
- Valerio Boncompagni, On hereditary graph classes defined by forbidding Truemper configurations (PhD thesis, 2018) (standard reference, not scraped)