Paths in acyclic simple graphs

This file records reusable consequences of acyclicity for paths in simple graphs.

Main results

• SimpleGraph.IsAcyclic.not_adj_getVert_of_add_one_lt: nonconsecutive vertices of a path in an acyclic graph are not adjacent.
• SimpleGraph.IsAcyclic.ne_of_adj_start_of_adj_end: an off-path neighbour of a path's start differs from every neighbour of its end.
• SimpleGraph.IsAcyclic.not_adj_of_adj_start_of_adj_end: when both lie off the path, such a neighbour of the start and a neighbour of the end are not adjacent.

theorem SimpleGraph.IsAcyclic.not_adj_getVert_of_add_one_lt {V : Type u_1} {G : SimpleGraph V} {u v : V} (hG : G.IsAcyclic) {p : G.Walk u v} (hp : p.IsPath) {i j : ℕ} (hij : i + 1 < j) (hj : j ≤ p.length) : ¬G.Adj (p.getVert i) (p.getVert j)

A path in an acyclic graph has no chord: vertices separated by at least one intermediate vertex cannot be adjacent.

theorem SimpleGraph.IsAcyclic.ne_of_adj_start_of_adj_end {V : Type u_1} {G : SimpleGraph V} {u v : V} (hG : G.IsAcyclic) (huv : u ≠ v) {q : G.Walk u v} (hq : q.IsPath) {a b : V} (ha : G.Adj u a) (ha' : a ∉ q.support) (hb : G.Adj v b) : a ≠ b

An off-path neighbour of a path's start differs from every neighbour of its end. In an acyclic graph, for a path with distinct endpoints. Only the start-side vertex is required to lie off the path; the end-side one is unconstrained.

theorem SimpleGraph.IsAcyclic.not_adj_of_adj_start_of_adj_end {V : Type u_1} {G : SimpleGraph V} {u v : V} (hG : G.IsAcyclic) {q : G.Walk u v} (hq : q.IsPath) {a b : V} (ha : G.Adj u a) (ha' : a ∉ q.support) (hb : G.Adj v b) (hb' : b ∉ q.support) : ¬G.Adj a b

Neighbours of a path's two ends, both lying off the path, are not adjacent. In an acyclic graph, no edge joins a vertex adjacent to the start of a path to one adjacent to its end. Here both are required to lie off the path, unlike in ne_of_adj_start_of_adj_end.