TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-01

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.

For every forest, $|V|=|E|+c$ , where $c$ is the number of connected components

Statement

If $F$ is a forest, let $\mathscr C(F)$ be the family of vertex sets of its connected components and put $c(F):=|\mathscr C(F)|$ . Then

$|V(F)|=|E(F)|+c(F).$

For the null forest, $c(F)=0$ .

Facts & Assumptions

Given: A finite forest $F$ .

[L1]

A forest contains no cycle, and a nonempty forest has a vertex of degree zero or one (Trees, forests, leaves and isolated vertices, Every nonempty forest has a vertex of degree at most one).

[L2]

Connected components partition the vertex set. Their vertex sets form a subset of the finite power set $\mathcal P(V(F))$ , so $\mathscr C(F)$ is finite and $c(F)$ is defined (The connected components of a graph partition its vertex set and are its maximal connected subgraphs, $\lvert\mathcal{P}(A)\rvert = 2^{\lvert A\rvert}$ for finite $A$ , A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$ , and equality holds if and only if $B = A$ , The cardinality $\lvert A\rvert$ of a finite set).

[F1]

Deleting a vertex deletes exactly its incident edges (Vertex and edge deletion, edge contraction, graph minors, subdivisions and topological minors).

[F2]

Finite disjoint unions obey the sum rule, and natural addition is associative and commutative (The cardinality $\lvert A\rvert$ of a finite set, The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , and a sum over a finite index set splits along a partition, Addition is associative, Addition is commutative).

[L3]

Induction is valid on $|V(F)|$ (The principle of mathematical induction).

Proof

technique · induction on $|V(F)|$

1.1

If $|V(F)|=0$ , then $|E(F)|=0$ and $c(F)=0$ , so the identity holds.

base

1.2

Let $|V(F)|>0$ , assume the identity for forests with fewer vertices, and choose a vertex $v$ of degree at most one.

ihL1L3

2.1

Put $F':=F-v$ . It remains a forest, and $V(F)$ is the disjoint union of $V(F')$ and $\{v\}$ , so $|V(F)|=|V(F')|+1$ .

step 1.2L1F1F2

3.1

If $v$ is isolated, then $E(F)=E(F')$ , while the component family of $F$ is the disjoint union of the component family of $F'$ and $\{\{v\}\}$ . Hence $|E(F)|=|E(F')|$ and $c(F)=c(F')+1$ .

step 2.1F1L2F2

3.2

If $v$ has degree one, deleting it removes its unique incident edge, so $|E(F)|=|E(F')|+1$ . It does not change the number of components: $v$ cannot be an internal vertex of a path between remaining vertices, and its neighbour remains in the same nonempty component after deletion. Thus $c(F)=c(F')$ .

step 2.1F1L2F2

4.1

In the isolated case, the induction hypothesis gives $|V(F)|=|V(F')|+1=(|E(F')|+c(F'))+1=|E(F)|+c(F)$ .

step 1.2step 2.1step 3.1F2

4.2

In the degree-one case, the induction hypothesis gives $|V(F)|=|V(F')|+1=(|E(F')|+c(F'))+1=(|E(F')|+1)+c(F')=|E(F)|+c(F)$ .

step 1.2step 2.1step 3.2F2

5.1

The two possible degrees of $v$ have both been handled, so the identity holds for every forest.

step 4.1step 4.2discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 82 results over 25 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)
ISI Bangalore discrete mathematics notes, Trees and Cayley’s theorem (standard reference, not scraped)

For every forest, ∣V∣=∣E∣+c|V|=|E|+c∣V∣=∣E∣+c, where ccc is the number of connected components