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 finite graph is connected if and only if it has a spanning tree
Statement
A finite graph is connected if and only if it has a spanning tree.
Facts & Assumptions
Given: A finite graph .
Every maximal acyclic spanning subgraph of a connected graph is a spanning tree (A maximal acyclic spanning subgraph of a connected graph is a spanning tree).
A spanning tree is a connected spanning subgraph (Spanning trees of a graph).
A finite graph has only finitely many edge subsets, so the family of acyclic spanning subgraphs has a maximal member.
A graph is connected when every two vertices are joined by a path (Connected graphs and connected components defined by the existence of vertex paths).
Proof
If is connected, choose a maximal acyclic spanning subgraph ; the edgeless spanning subgraph shows that the choice family is nonempty.
By L1, is a spanning tree of .
Conversely, if has a spanning tree , every two vertices are joined by a path in , hence by a path in . Thus is connected.
Depends on
Used by
- For a plane graph with c components, |V|-|E|+|F|=1+c, including the null graph Corollary
- Real edge-weighted graphs, total tree weight and minimum spanning trees Definition
- A connected graph with two distinct spanning trees Example
- Euler's formula |V|-|E|+|F|=2 for every connected plane graph Theorem
- Kruskal's greedy edge procedure produces a minimum spanning tree Theorem
- Prim's growing-tree procedure produces a minimum spanning tree Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 32 results over 16 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
- Reinhard Diestel, Graph Theory, Preview Chapter 1 (standard reference, not scraped)