Paths, cycles and connectivity

Walks, paths and cycles in graphs, Eulerian and Hamiltonian cycles, and vertex and edge connectivity, including Menger's theorem and Fleischner's theorem on squares of 2-connected graphs.

• Bridges and bridgeless graphs
• Cycle covers
• Cycle lengths and circumference
• Eulerian circuits
• Menger's theorem
• Reachability and connectedness
• Vertex connectivity
• Hamiltonian cycles
• Square of a graph
• Říha's cycle lemma
• Fleischner's theorem

TheoremConcatenation of paths meeting at one endpoint is a path#✓fully proved

Two paths that meet only at their common endpoint m concatenate to a path.

theorem isPath_append_of_isPath {V : Type*} {G : SimpleGraph V} {u m v : V}
    {p : G.Walk u m} {q : G.Walk m v} (hp : p.IsPath) (hq : q.IsPath)
    (hi : ∀ a ∈ p.support, a ∈ q.support → a = m) : (p.append q).IsPath

Used by 2

Used byClusters seen from a leaf are edge sides · Tree metrics satisfy the four-point condition

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.