Theorems · Inductive type · combinatorics

SimpleGraph.Walk

{V : Type u} → SimpleGraph V → V → V → Type u

A walk is a sequence of adjacent vertices. For vertices u v : V, the type walk u v consists of all walks starting at u and ending at v. We say that a walk visits the vertices it contains. The set of vertices a walk visits is SimpleGraph.Walk.support. See SimpleGraph.Walk.nil' and SimpleGraph.Walk.cons' for patterns that can be useful in definitions since they make the vertices explicit.

Defined in

Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Cited by

915 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms