Trees

A tree is a connected graph in which no edge lies on a cycle. What the blueprint asks of a tree is always about its leaves, and every such question starts the same way: take a longest path. Neither of its ends can carry a second edge — an edge back onto the path would close a cycle, and an edge off the path would make a longer path — so both ends are leaves.

The three theorems this file exists for

• deleting a leaf leaves a tree (Graph.IsTree.delete_leaf),
• a tree on n vertices has n - 1 edges (Graph.IsTree.edge_count), by peeling leaves,
• a tree with exactly three leaves has one vertex of degree three (Graph.IsTree.three_leaves), which is where the handshake lemma finally pays.

Why a longest path rather than a maximal one

A longest path is produced by Nat.findGreatest over the lengths of paths, bounded because a path repeats no edge (Graph.IsPath.nodup) and the graph has finitely many. That needs Graph.Finite and nothing else — in particular no well-founded recursion and no choice of a maximal element in an order. The bound is the only place finiteness enters the longest-path argument.

Vertex deletion

Graph.deleteVerts is Mathlib's. What this file adds is the transfer lemma every deletion argument reduces to — Graph.IsWalk.deleteVerts, a walk that never visits a deleted vertex survives — together with the reason the hypothesis is ever available: Graph.IsLeaf.path_avoids, a path whose two ends are elsewhere never visits a vertex of degree one. To pass through such a vertex a path would have to arrive and leave along its single edge, and a path takes no edge twice.

Blueprint

• Graph.IsTree.three_leaves — lem:three-leaf-tree ("a finite tree with exactly three leaves has exactly one vertex of degree at least three; that vertex has degree exactly three, and every other vertex is a leaf or has degree two"), used at the H5 step of lem:two-components to produce the three internally disjoint branches of each spanning tree T_i.
• Graph.IsTree.edge_count — the same lemma's "a finite tree with n vertices has exactly n - 1 edges".
• Graph.IsTree.has_leaf, Graph.IsTree.delete_leaf — its "a tree with an edge has a leaf, since an endpoint of a maximal simple path has no neighbor off the path, and a second neighbor on the path would close a cycle; deleting a leaf and its edge leaves a tree".
• Graph.IsTree — the trees of lem:two-components ("take a minimal connected subgraph T_i spanning the three terminals. It is a tree").

Namespace

The root Graph namespace, as in Walk.lean, Degree.lean and Cycle.lean.

Trees

def Graph.IsTree {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

G.IsTree : a connected graph in which no edge lies on a cycle. Connectedness carries nonemptiness (Graph.Connected), which is what makes the counting statements below true as stated.

Equations

• G.IsTree = (G.Connected ∧ G.IsAcyclic)

theorem Graph.IsTree.connected {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsTree) : G.Connected

theorem Graph.IsTree.isAcyclic {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsTree) : G.IsAcyclic

theorem Graph.isTree_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsTree ↔ G.Connected ∧ G.IsAcyclic

A walk departs along an edge

theorem Graph.IsWalk.exists_inc_source {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) (hW : W ≠ []) : ∃ e ∈ W, G.Inc e u

A walk that gets anywhere leaves along an edge at its source.

theorem Graph.IsPath.ne_nil {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {P : List β} (h : G.IsPath u P v) (huv : u ≠ v) : P ≠ []

A path between two distinct vertices takes at least one edge.

theorem Graph.Connected.degree_pos {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] (hG : G.Connected) (h2 : 2 ≤ G.vertexSet.ncard) (hx : x ∈ G.vertexSet) : 0 < G.degree x

In a connected graph on two or more vertices nothing is isolated.

A path leaves its source once and for all

Two edges of a path incident with its source are the same edge: the departing step is the only candidate, since a later edge at the source would put the source back among the vertices the rest of the path visits.

theorem Graph.IsPath.eq_head_of_inc_source {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e f : β} {W : List β} (h : G.IsPath u (e :: W) v) (hf : f ∈ e :: W) (hinc : G.Inc f u) : f = e

An edge of a path incident with the path's source is the one the path departs along.

theorem Graph.IsPath.inc_source_unique {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e f : β} {P : List β} (h : G.IsPath u P v) (hf : f ∈ P) (he : e ∈ P) (hfi : G.Inc f u) (hei : G.Inc e u) : f = e

A path has at most one edge at its source.

A longest path

theorem Graph.IsPath.length_le_ncard_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {P : List β} [G.Finite] (h : G.IsPath u P v) : P.length ≤ G.edgeSet.ncard

A path repeats no edge, so it is no longer than the graph has edges.

theorem Graph.exists_longest_path {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} [G.Finite] (hu : u ∈ G.vertexSet) : ∃ (x : α) (y : α) (Q : List β), G.IsPath x Q y ∧ ∀ (x' y' : α) (Q' : List β), G.IsPath x' Q' y' → Q'.length ≤ Q.length

A finite graph with a vertex has a longest path. The lengths of paths are bounded by the number of edges, so Nat.findGreatest picks the largest length that occurs, and the witnessing path is longest.

Both ends of a longest path are leaves

theorem Graph.IsAcyclic.longest_path_source_edge {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {P : List β} (hac : G.IsAcyclic) (hP : G.IsPath u P v) (hlong : ∀ (x' y' : α) (Q : List β), G.IsPath x' Q y' → Q.length ≤ P.length) (hinc : G.Inc e u) : e ∈ P

Every edge at the source of a longest path is one of the path's own edges. The two ways out are both closed: an edge onto a vertex the path visits closes a cycle (Graph.IsAcyclic.mem_of_isLink_of_mem_walkVertices), and an edge to a vertex it does not visit extends the path.

theorem Graph.IsAcyclic.longest_path_source_is_leaf {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {P : List β} (hac : G.IsAcyclic) (hP : G.IsPath u P v) (hlong : ∀ (x' y' : α) (Q : List β), G.IsPath x' Q y' → Q.length ≤ P.length) (hinc : G.Inc e u) : G.IsLeaf u

The source of a longest path in an acyclic graph is a leaf, as soon as it carries an edge at all: every edge there is one of the path's, and the path leaves the vertex only once, so they are all the same edge.

theorem Graph.IsAcyclic.longest_path_target_is_leaf {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {P : List β} (hac : G.IsAcyclic) (hP : G.IsPath u P v) (hlong : ∀ (x' y' : α) (Q : List β), G.IsPath x' Q y' → Q.length ≤ P.length) (hinc : G.Inc e v) : G.IsLeaf v

The target of a longest path in an acyclic graph is a leaf too: reversing a path preserves its length, so the reverse is longest as well.

theorem Graph.IsTree.has_leaf {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (hT : G.IsTree) (h2 : 2 ≤ G.vertexSet.ncard) : ∃ (x : α), G.IsLeaf x

A tree on two or more vertices has a leaf. Two distinct vertices are joined by a path that takes an edge, so a longest path takes one too, and its source is a leaf.

A path steers clear of a leaf

theorem Graph.IsLeaf.path_avoids {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} {P : List β} [G.Finite] (hx : G.IsLeaf x) (hP : G.IsPath u P v) : u ≠ x → v ≠ x → x ∉ G.walkVertices u P

A path whose two ends are elsewhere never visits a vertex of degree one. To pass through such a vertex the path would have to arrive and leave along that vertex's single edge, and a path takes no edge twice. This is what makes connectivity survive the deletion of a leaf.

Vertex deletion

theorem Graph.IsWalk.deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} {X : Set α} (h : G.IsWalk u W v) (hX : ∀ z ∈ G.walkVertices u W, z ∉ X) : (G.deleteVerts X).IsWalk u W v

A walk that visits no deleted vertex survives the deletion. Both ends of each of its edges are vertices it visits, so they too survive.

theorem Graph.edgeSet_deleteVerts_singleton {α : Type u_1} {β : Type u_2} (G : Graph α β) (x : α) : (G.deleteVerts {x}).edgeSet = G.edgeSet \ incidenceSet x

Deleting a vertex removes exactly the edges that meet it.

theorem Graph.IsTree.delete_leaf {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} [G.Finite] (hT : G.IsTree) (hx : G.IsLeaf x) (h2 : 2 ≤ G.vertexSet.ncard) : (G.deleteVerts {x}).IsTree

A tree minus a leaf is a tree. Acyclicity is inherited by every subgraph; connectedness survives because every path between two surviving vertices already steered clear of the leaf (Graph.IsLeaf.path_avoids).

A tree has one edge fewer than it has vertices

theorem Graph.IsTree.edge_count {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (hT : G.IsTree) : G.edgeSet.ncard + 1 = G.vertexSet.ncard

A tree has one edge fewer than it has vertices.

A tree with three leaves

The blueprint's lem:three-leaf-tree, and the one place the handshake lemma is used. Three leaves contribute one apiece to the degree sum, every other vertex contributes two plus whatever it carries above two, and the totals leave exactly one degree to carry.

theorem Graph.IsTree.three_leaves {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (hT : G.IsTree) (hleaves : {z : α | G.IsLeaf z}.ncard = 3) : ∃ x ∈ G.vertexSet, G.degree x = 3 ∧ ∀ z ∈ G.vertexSet, z ≠ x → G.degree z ≤ 2

A tree with exactly three leaves has a vertex of degree three, and every other vertex has degree at most two — so it is a leaf or has degree exactly two, and the vertex of degree three is unique.

The count: with k non-leaf vertices the tree has k + 3 vertices, hence k + 2 edges (Graph.IsTree.edge_count), hence degree sum 2k + 4 (the handshake lemma). The leaves contribute 3, so the non-leaves contribute 2k + 1; each contributes at least 2, so between them they carry exactly one degree above two.