# mathlib3documentation

combinatorics.simple_graph.connectivity

# Graph connectivity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In a simple graph,

• A walk is a finite sequence of adjacent vertices, and can be thought of equally well as a sequence of directed edges.

• A trail is a walk whose edges each appear no more than once.

• A path is a trail whose vertices appear no more than once.

• A cycle is a nonempty trail whose first and last vertices are the same and whose vertices except for the first appear no more than once.

Warning: graph theorists mean something different by "path" than do homotopy theorists. A "walk" in graph theory is a "path" in homotopy theory. Another warning: some graph theorists use "path" and "simple path" for "walk" and "path."

Some definitions and theorems have inspiration from multigraph counterparts in [Cho94].

## Main definitions #

• `simple_graph.walk` (with accompanying pattern definitions `simple_graph.walk.nil'` and `simple_graph.walk.cons'`)

• `simple_graph.walk.is_trail`, `simple_graph.walk.is_path`, and `simple_graph.walk.is_cycle`.

• `simple_graph.path`

• `simple_graph.walk.map` and `simple_graph.path.map` for the induced map on walks, given an (injective) graph homomorphism.

• `simple_graph.reachable` for the relation of whether there exists a walk between a given pair of vertices

• `simple_graph.preconnected` and `simple_graph.connected` are predicates on simple graphs for whether every vertex can be reached from every other, and in the latter case, whether the vertex type is nonempty.

• `simple_graph.subgraph.connected` gives subgraphs the connectivity predicate via `simple_graph.subgraph.coe`.

• `simple_graph.connected_component` is the type of connected components of a given graph.

• `simple_graph.is_bridge` for whether an edge is a bridge edge

## Main statements #

• `simple_graph.is_bridge_iff_mem_and_forall_cycle_not_mem` characterizes bridge edges in terms of there being no cycle containing them.

## Tags #

walks, trails, paths, circuits, cycles, bridge edges

inductive simple_graph.walk {V : Type u} (G : simple_graph 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 `simple_graph.walk.support`.

See `simple_graph.walk.nil'` and `simple_graph.walk.cons'` for patterns that can be useful in definitions since they make the vertices explicit.

Instances for `simple_graph.walk`
@[protected, instance]
def simple_graph.walk.decidable_eq {V : Type u} [a : decidable_eq V] (G : simple_graph V) (ᾰ ᾰ_1 : V) :
decidable_eq (G.walk ᾰ_1)
@[protected, instance]
def simple_graph.walk.inhabited {V : Type u} (G : simple_graph V) (v : V) :
inhabited (G.walk v v)
Equations
@[simp]
theorem simple_graph.walk.inhabited_default {V : Type u} (G : simple_graph V) (v : V) :
@[reducible]
def simple_graph.adj.to_walk {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
G.walk u v

The one-edge walk associated to a pair of adjacent vertices.

Equations
@[reducible]
def simple_graph.walk.nil' {V : Type u} {G : simple_graph V} (u : V) :
G.walk u u

Pattern to get `walk.nil` with the vertex as an explicit argument.

@[reducible]
def simple_graph.walk.cons' {V : Type u} {G : simple_graph V} (u v w : V) (h : G.adj u v) (p : G.walk v w) :
G.walk u w

Pattern to get `walk.cons` with the vertices as explicit arguments.

@[protected]
def simple_graph.walk.copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
G.walk u' v'

Change the endpoints of a walk using equalities. This is helpful for relaxing definitional equality constraints and to be able to state otherwise difficult-to-state lemmas. While this is a simple wrapper around `eq.rec`, it gives a canonical way to write it.

The simp-normal form is for the `copy` to be pushed outward. That way calculations can occur within the "copy context."

Equations
• p.copy hu hv = eq.rec (eq.rec p hv) hu
@[simp]
theorem simple_graph.walk.copy_rfl_rfl {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.copy_copy {V : Type u} {G : simple_graph V} {u v u' v' u'' v'' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') :
(p.copy hu hv).copy hu' hv' = p.copy _ _
@[simp]
theorem simple_graph.walk.copy_nil {V : Type u} {G : simple_graph V} {u u' : V} (hu : u = u') :
theorem simple_graph.walk.copy_cons {V : Type u} {G : simple_graph V} {u v w u' w' : V} (h : G.adj u v) (p : G.walk v w) (hu : u = u') (hw : w = w') :
.copy hu hw = (p.copy rfl hw)
@[simp]
theorem simple_graph.walk.cons_copy {V : Type u} {G : simple_graph V} {u v w v' w' : V} (h : G.adj u v) (p : G.walk v' w') (hv : v' = v) (hw : w' = w) :
(p.copy hv hw) = hw
theorem simple_graph.walk.exists_eq_cons_of_ne {V : Type u} {G : simple_graph V} {u v : V} (hne : u v) (p : G.walk u v) :
(w : V) (h : G.adj u w) (p' : G.walk w v), p =
def simple_graph.walk.length {V : Type u} {G : simple_graph V} {u v : V} :
G.walk u v

The length of a walk is the number of edges/darts along it.

Equations
@[trans]
def simple_graph.walk.append {V : Type u} {G : simple_graph V} {u v w : V} :
G.walk u v G.walk v w G.walk u w

The concatenation of two compatible walks.

Equations
def simple_graph.walk.concat {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
G.walk u w

The reversed version of `simple_graph.walk.cons`, concatenating an edge to the end of a walk.

Equations
theorem simple_graph.walk.concat_eq_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
@[protected]
def simple_graph.walk.reverse_aux {V : Type u} {G : simple_graph V} {u v w : V} :
G.walk u v G.walk u w G.walk v w

The concatenation of the reverse of the first walk with the second walk.

Equations
@[symm]
def simple_graph.walk.reverse {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) :
G.walk v u

The walk in reverse.

Equations
def simple_graph.walk.get_vert {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) (n : ) :
V

Get the `n`th vertex from a walk, where `n` is generally expected to be between `0` and `p.length`, inclusive. If `n` is greater than or equal to `p.length`, the result is the path's endpoint.

Equations
@[simp]
theorem simple_graph.walk.get_vert_zero {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) :
w.get_vert 0 = u
theorem simple_graph.walk.get_vert_of_length_le {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) {i : } (hi : w.length i) :
w.get_vert i = v
@[simp]
theorem simple_graph.walk.get_vert_length {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) :
theorem simple_graph.walk.adj_get_vert_succ {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) {i : } (hi : i < w.length) :
G.adj (w.get_vert i) (w.get_vert (i + 1))
@[simp]
theorem simple_graph.walk.cons_append {V : Type u} {G : simple_graph V} {u v w x : V} (h : G.adj u v) (p : G.walk v w) (q : G.walk w x) :
.append q = (p.append q)
@[simp]
theorem simple_graph.walk.cons_nil_append {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
@[simp]
theorem simple_graph.walk.append_nil {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.nil_append {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.append_assoc {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk v w) (r : G.walk w x) :
p.append (q.append r) = (p.append q).append r
@[simp]
theorem simple_graph.walk.append_copy_copy {V : Type u} {G : simple_graph V} {u v w u' v' w' : V} (p : G.walk u v) (q : G.walk v w) (hu : u = u') (hv : v = v') (hw : w = w') :
(p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw
theorem simple_graph.walk.concat_nil {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
@[simp]
theorem simple_graph.walk.concat_cons {V : Type u} {G : simple_graph V} {u v w x : V} (h : G.adj u v) (p : G.walk v w) (h' : G.adj w x) :
.concat h' = (p.concat h')
theorem simple_graph.walk.append_concat {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk v w) (h : G.adj w x) :
p.append (q.concat h) = (p.append q).concat h
theorem simple_graph.walk.concat_append {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (h : G.adj v w) (q : G.walk w x) :
(p.concat h).append q = p.append
theorem simple_graph.walk.exists_cons_eq_concat {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
(x : V) (q : G.walk u x) (h' : G.adj x w), = q.concat h'

A non-trivial `cons` walk is representable as a `concat` walk.

theorem simple_graph.walk.exists_concat_eq_cons {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
(x : V) (h' : G.adj u x) (q : G.walk x w), p.concat h =

A non-trivial `concat` walk is representable as a `cons` walk.

@[simp]
theorem simple_graph.walk.reverse_nil {V : Type u} {G : simple_graph V} {u : V} :
theorem simple_graph.walk.reverse_singleton {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
@[simp]
theorem simple_graph.walk.cons_reverse_aux {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk w x) (h : G.adj w u) :
=
@[protected, simp]
theorem simple_graph.walk.append_reverse_aux {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk v w) (r : G.walk u x) :
@[protected, simp]
theorem simple_graph.walk.reverse_aux_append {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk u w) (r : G.walk w x) :
@[protected]
theorem simple_graph.walk.reverse_aux_eq_reverse_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk u w) :
@[simp]
theorem simple_graph.walk.reverse_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
@[simp]
theorem simple_graph.walk.reverse_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).reverse = p.reverse.copy hv hu
@[simp]
theorem simple_graph.walk.reverse_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
@[simp]
theorem simple_graph.walk.reverse_concat {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
@[simp]
theorem simple_graph.walk.reverse_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.length_nil {V : Type u} {G : simple_graph V} {u : V} :
@[simp]
theorem simple_graph.walk.length_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
@[simp]
theorem simple_graph.walk.length_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).length = p.length
@[simp]
theorem simple_graph.walk.length_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
@[simp]
theorem simple_graph.walk.length_concat {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
(p.concat h).length = p.length + 1
@[protected, simp]
theorem simple_graph.walk.length_reverse_aux {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk u w) :
@[simp]
theorem simple_graph.walk.length_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.eq_of_length_eq_zero {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} :
p.length = 0 u = v
@[simp]
theorem simple_graph.walk.exists_length_eq_zero_iff {V : Type u} {G : simple_graph V} {u v : V} :
( (p : G.walk u v), p.length = 0) u = v
@[simp]
theorem simple_graph.walk.length_eq_zero_iff {V : Type u} {G : simple_graph V} {u : V} {p : G.walk u u} :
p.length = 0
def simple_graph.walk.concat_rec_aux {V : Type u} {G : simple_graph V} {motive : Π (u v : V), G.walk u v Sort u_1} (Hnil : Π {u : V}, motive u u simple_graph.walk.nil) (Hconcat : Π {u v w : V} (p : G.walk u v) (h : G.adj v w), motive u v p motive u w (p.concat h)) {u v : V} (p : G.walk u v) :
motive v u p.reverse

Auxiliary definition for `simple_graph.walk.concat_rec`

Equations
• Hconcat = eq.rec (Hconcat p.reverse _ Hconcat p)) _
• = Hnil
def simple_graph.walk.concat_rec {V : Type u} {G : simple_graph V} {motive : Π (u v : V), G.walk u v Sort u_1} (Hnil : Π {u : V}, motive u u simple_graph.walk.nil) (Hconcat : Π {u v w : V} (p : G.walk u v) (h : G.adj v w), motive u v p motive u w (p.concat h)) {u v : V} (p : G.walk u v) :
motive u v p

Recursor on walks by inducting on `simple_graph.walk.concat`.

This is inducting from the opposite end of the walk compared to `simple_graph.walk.rec`, which inducts on `simple_graph.walk.cons`.

Equations
• Hconcat p = eq.rec Hconcat p.reverse) _
@[simp]
theorem simple_graph.walk.concat_rec_nil {V : Type u} {G : simple_graph V} {motive : Π (u v : V), G.walk u v Sort u_1} (Hnil : Π {u : V}, motive u u simple_graph.walk.nil) (Hconcat : Π {u v w : V} (p : G.walk u v) (h : G.adj v w), motive u v p motive u w (p.concat h)) (u : V) :
Hconcat simple_graph.walk.nil = Hnil
@[simp]
theorem simple_graph.walk.concat_rec_concat {V : Type u} {G : simple_graph V} {motive : Π (u v : V), G.walk u v Sort u_1} (Hnil : Π {u : V}, motive u u simple_graph.walk.nil) (Hconcat : Π {u v w : V} (p : G.walk u v) (h : G.adj v w), motive u v p motive u w (p.concat h)) {u v w : V} (p : G.walk u v) (h : G.adj v w) :
Hconcat (p.concat h) = Hconcat p h Hconcat p)
theorem simple_graph.walk.concat_ne_nil {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) (h : G.adj v u) :
theorem simple_graph.walk.concat_inj {V : Type u} {G : simple_graph V} {u v v' w : V} {p : G.walk u v} {h : G.adj v w} {p' : G.walk u v'} {h' : G.adj v' w} (he : p.concat h = p'.concat h') :
(hv : v = v'), p.copy rfl hv = p'
def simple_graph.walk.support {V : Type u} {G : simple_graph V} {u v : V} :
G.walk u v list V

The `support` of a walk is the list of vertices it visits in order.

Equations
def simple_graph.walk.darts {V : Type u} {G : simple_graph V} {u v : V} :
G.walk u v list G.dart

The `darts` of a walk is the list of darts it visits in order.

Equations
def simple_graph.walk.edges {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :

The `edges` of a walk is the list of edges it visits in order. This is defined to be the list of edges underlying `simple_graph.walk.darts`.

Equations
@[simp]
theorem simple_graph.walk.support_nil {V : Type u} {G : simple_graph V} {u : V} :
@[simp]
theorem simple_graph.walk.support_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
= u :: p.support
@[simp]
theorem simple_graph.walk.support_concat {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
@[simp]
theorem simple_graph.walk.support_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).support = p.support
theorem simple_graph.walk.support_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
@[simp]
theorem simple_graph.walk.support_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.support_ne_nil {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.tail_support_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
theorem simple_graph.walk.support_eq_cons {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.start_mem_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.end_mem_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.support_nonempty {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
{w : V | w p.support}.nonempty
theorem simple_graph.walk.mem_support_iff {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) :
theorem simple_graph.walk.mem_support_nil_iff {V : Type u} {G : simple_graph V} {u v : V} :
u = v
@[simp]
theorem simple_graph.walk.mem_tail_support_append_iff {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk u v) (p' : G.walk v w) :
@[simp]
theorem simple_graph.walk.end_mem_tail_support_of_ne {V : Type u} {G : simple_graph V} {u v : V} (h : u v) (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.mem_support_append_iff {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk u v) (p' : G.walk v w) :
@[simp]
theorem simple_graph.walk.subset_support_append_left {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
@[simp]
theorem simple_graph.walk.subset_support_append_right {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
theorem simple_graph.walk.coe_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.coe_support_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
theorem simple_graph.walk.coe_support_append' {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
((p.append p').support) = (p.support) + (p'.support) - {v}
theorem simple_graph.walk.chain_adj_support {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
u p.support
theorem simple_graph.walk.chain'_adj_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.chain_dart_adj_darts {V : Type u} {G : simple_graph V} {d : G.dart} {v w : V} (h : d.to_prod.snd = v) (p : G.walk v w) :
theorem simple_graph.walk.chain'_dart_adj_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.edges_subset_edge_set {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) ⦃e : sym2 V⦄ (h : e p.edges) :

Every edge in a walk's edge list is an edge of the graph. It is written in this form (rather than using `⊆`) to avoid unsightly coercions.

theorem simple_graph.walk.adj_of_mem_edges {V : Type u} {G : simple_graph V} {u v x y : V} (p : G.walk u v) (h : (x, y) p.edges) :
@[simp]
theorem simple_graph.walk.darts_nil {V : Type u} {G : simple_graph V} {u : V} :
@[simp]
theorem simple_graph.walk.darts_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
.darts = {to_prod := (u, v), is_adj := h} :: p.darts
@[simp]
theorem simple_graph.walk.darts_concat {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
(p.concat h).darts = p.darts.concat {to_prod := (v, w), is_adj := h}
@[simp]
theorem simple_graph.walk.darts_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).darts = p.darts
@[simp]
theorem simple_graph.walk.darts_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
(p.append p').darts = p.darts ++ p'.darts
@[simp]
theorem simple_graph.walk.darts_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.mem_darts_reverse {V : Type u} {G : simple_graph V} {u v : V} {d : G.dart} {p : G.walk u v} :
theorem simple_graph.walk.cons_map_snd_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.map_snd_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.map_fst_darts_append {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.map_fst_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.edges_nil {V : Type u} {G : simple_graph V} {u : V} :
@[simp]
theorem simple_graph.walk.edges_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
.edges = (u, v) :: p.edges
@[simp]
theorem simple_graph.walk.edges_concat {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
@[simp]
theorem simple_graph.walk.edges_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).edges = p.edges
@[simp]
theorem simple_graph.walk.edges_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
(p.append p').edges = p.edges ++ p'.edges
@[simp]
theorem simple_graph.walk.edges_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.length_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.length_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.length_edges {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.dart_fst_mem_support_of_mem_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {d : G.dart} :
theorem simple_graph.walk.dart_snd_mem_support_of_mem_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {d : G.dart} (h : d p.darts) :
theorem simple_graph.walk.fst_mem_support_of_mem_edges {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk v w) (he : (t, u) p.edges) :
theorem simple_graph.walk.snd_mem_support_of_mem_edges {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk v w) (he : (t, u) p.edges) :
theorem simple_graph.walk.darts_nodup_of_support_nodup {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.support.nodup) :
theorem simple_graph.walk.edges_nodup_of_support_nodup {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.support.nodup) :

### Trails, paths, circuits, cycles #

structure simple_graph.walk.is_trail {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
Prop

A trail is a walk with no repeating edges.

structure simple_graph.walk.is_path {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
Prop

A path is a walk with no repeating vertices. Use `simple_graph.walk.is_path.mk'` for a simpler constructor.

Instances for `simple_graph.walk.is_path`
structure simple_graph.walk.is_circuit {V : Type u} {G : simple_graph V} {u : V} (p : G.walk u u) :
Prop

A circuit at `u : V` is a nonempty trail beginning and ending at `u`.

structure simple_graph.walk.is_cycle {V : Type u} {G : simple_graph V} {u : V} (p : G.walk u u) :
Prop

A cycle at `u : V` is a circuit at `u` whose only repeating vertex is `u` (which appears exactly twice).

theorem simple_graph.walk.is_trail_def {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.is_trail_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
theorem simple_graph.walk.is_path.mk' {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.support.nodup) :
theorem simple_graph.walk.is_path_def {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.is_path_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).is_path p.is_path
theorem simple_graph.walk.is_circuit_def {V : Type u} {G : simple_graph V} {u : V} (p : G.walk u u) :
@[simp]
theorem simple_graph.walk.is_circuit_copy {V : Type u} {G : simple_graph V} {u u' : V} (p : G.walk u u) (hu : u = u') :
theorem simple_graph.walk.is_cycle_def {V : Type u} {G : simple_graph V} {u : V} (p : G.walk u u) :
@[simp]
theorem simple_graph.walk.is_cycle_copy {V : Type u} {G : simple_graph V} {u u' : V} (p : G.walk u u) (hu : u = u') :
@[simp]
theorem simple_graph.walk.is_trail.nil {V : Type u} {G : simple_graph V} {u : V} :
theorem simple_graph.walk.is_trail.of_cons {V : Type u} {G : simple_graph V} {u v w : V} {h : G.adj u v} {p : G.walk v w} :
@[simp]
theorem simple_graph.walk.cons_is_trail_iff {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
theorem simple_graph.walk.is_trail.reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) (h : p.is_trail) :
@[simp]
theorem simple_graph.walk.reverse_is_trail_iff {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.is_trail.of_append_left {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} (h : (p.append q).is_trail) :
theorem simple_graph.walk.is_trail.of_append_right {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} (h : (p.append q).is_trail) :
theorem simple_graph.walk.is_trail.count_edges_le_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_trail) (e : sym2 V) :
p.edges 1
theorem simple_graph.walk.is_trail.count_edges_eq_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_trail) {e : sym2 V} (he : e p.edges) :
p.edges = 1
theorem simple_graph.walk.is_path.nil {V : Type u} {G : simple_graph V} {u : V} :
theorem simple_graph.walk.is_path.of_cons {V : Type u} {G : simple_graph V} {u v w : V} {h : G.adj u v} {p : G.walk v w} :
@[simp]
theorem simple_graph.walk.cons_is_path_iff {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
@[simp]
theorem simple_graph.walk.is_path_iff_eq_nil {V : Type u} {G : simple_graph V} {u : V} (p : G.walk u u) :
theorem simple_graph.walk.is_path.reverse {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.is_path) :
@[simp]
theorem simple_graph.walk.is_path_reverse_iff {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.is_path.of_append_left {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} :
theorem simple_graph.walk.is_path.of_append_right {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} (h : (p.append q).is_path) :
@[simp]
theorem simple_graph.walk.is_cycle.not_of_nil {V : Type u} {G : simple_graph V} {u : V} :
theorem simple_graph.walk.cons_is_cycle_iff {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk v u) (h : G.adj u v) :

@[protected, instance]
def simple_graph.walk.is_path.decidable {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
Equations
theorem simple_graph.walk.is_path.length_lt {V : Type u} {G : simple_graph V} [fintype V] {u v : V} {p : G.walk u v} (hp : p.is_path) :

### Walk decompositions #

def simple_graph.walk.take_until {V : Type u} {G : simple_graph V} [decidable_eq V] {v w : V} (p : G.walk v w) (u : V) (h : u p.support) :
G.walk v u

Given a vertex in the support of a path, give the path up until (and including) that vertex.

Equations
def simple_graph.walk.drop_until {V : Type u} {G : simple_graph V} [decidable_eq V] {v w : V} (p : G.walk v w) (u : V) (h : u p.support) :
G.walk u w

Given a vertex in the support of a path, give the path from (and including) that vertex to the end. In other words, drop vertices from the front of a path until (and not including) that vertex.

Equations
@[simp]
theorem simple_graph.walk.take_spec {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
(p.take_until u h).append (p.drop_until u h) = p

The `take_until` and `drop_until` functions split a walk into two pieces. The lemma `count_support_take_until_eq_one` specifies where this split occurs.

theorem simple_graph.walk.mem_support_iff_exists_append {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} :
w p.support (q : G.walk u w) (r : G.walk w v), p = q.append r
@[simp]
theorem simple_graph.walk.count_support_take_until_eq_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
(p.take_until u h).support = 1
theorem simple_graph.walk.count_edges_take_until_le_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) (x : V) :
@[simp]
theorem simple_graph.walk.take_until_copy {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w v' w' : V} (p : G.walk v w) (hv : v = v') (hw : w = w') (h : u (p.copy hv hw).support) :
(p.copy hv hw).take_until u h = (p.take_until u _).copy hv rfl
@[simp]
theorem simple_graph.walk.drop_until_copy {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w v' w' : V} (p : G.walk v w) (hv : v = v') (hw : w = w') (h : u (p.copy hv hw).support) :
(p.copy hv hw).drop_until u h = (p.drop_until u _).copy rfl hw
theorem simple_graph.walk.support_take_until_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
theorem simple_graph.walk.support_drop_until_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
theorem simple_graph.walk.darts_take_until_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
theorem simple_graph.walk.darts_drop_until_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
theorem simple_graph.walk.edges_take_until_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
theorem simple_graph.walk.edges_drop_until_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
theorem simple_graph.walk.length_take_until_le {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
theorem simple_graph.walk.length_drop_until_le {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (h : u p.support) :
@[protected]
theorem simple_graph.walk.is_trail.take_until {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} {p : G.walk v w} (hc : p.is_trail) (h : u p.support) :
@[protected]
theorem simple_graph.walk.is_trail.drop_until {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} {p : G.walk v w} (hc : p.is_trail) (h : u p.support) :
@[protected]
theorem simple_graph.walk.is_path.take_until {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} {p : G.walk v w} (hc : p.is_path) (h : u p.support) :
@[protected]
theorem simple_graph.walk.is_path.drop_until {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk v w) (hc : p.is_path) (h : u p.support) :
def simple_graph.walk.rotate {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (c : G.walk v v) (h : u c.support) :
G.walk u u

Rotate a loop walk such that it is centered at the given vertex.

Equations
@[simp]
theorem simple_graph.walk.support_rotate {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (c : G.walk v v) (h : u c.support) :
theorem simple_graph.walk.rotate_darts {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (c : G.walk v v) (h : u c.support) :
theorem simple_graph.walk.rotate_edges {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (c : G.walk v v) (h : u c.support) :
@[protected]
theorem simple_graph.walk.is_trail.rotate {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {c : G.walk v v} (hc : c.is_trail) (h : u c.support) :
@[protected]
theorem simple_graph.walk.is_circuit.rotate {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {c : G.walk v v} (hc : c.is_circuit) (h : u c.support) :
@[protected]
theorem simple_graph.walk.is_cycle.rotate {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {c : G.walk v v} (hc : c.is_cycle) (h : u c.support) :
theorem simple_graph.walk.exists_boundary_dart {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) (S : set V) (uS : u S) (vS : v S) :

Given a set `S` and a walk `w` from `u` to `v` such that `u ∈ S` but `v ∉ S`, there exists a dart in the walk whose start is in `S` but whose end is not.

### Type of paths #

@[reducible]
def simple_graph.path {V : Type u} (G : simple_graph V) (u v : V) :

The type for paths between two vertices.

@[protected, simp]
theorem simple_graph.path.is_path {V : Type u} {G : simple_graph V} {u v : V} (p : G.path u v) :
@[protected, simp]
theorem simple_graph.path.is_trail {V : Type u} {G : simple_graph V} {u v : V} (p : G.path u v) :
@[simp]
theorem simple_graph.path.nil_coe {V : Type u} {G : simple_graph V} {u : V} :
@[protected, refl]
def simple_graph.path.nil {V : Type u} {G : simple_graph V} {u : V} :
G.path u u

The length-0 path at a vertex.

Equations
def simple_graph.path.singleton {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
G.path u v

The length-1 path between a pair of adjacent vertices.

Equations
@[simp]
theorem simple_graph.path.singleton_coe {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
theorem simple_graph.path.mk_mem_edges_singleton {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
(u, v)
@[simp]
theorem simple_graph.path.reverse_coe {V : Type u} {G : simple_graph V} {u v : V} (p : G.path u v) :
@[symm]
def simple_graph.path.reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.path u v) :
G.path v u

The reverse of a path is another path. See also `simple_graph.walk.reverse`.

Equations
theorem simple_graph.path.count_support_eq_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} {p : G.path u v} (hw : w p.support) :
= 1
theorem simple_graph.path.count_edges_eq_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.path u v} (e : sym2 V) (hw : e p.edges) :
p.edges = 1
@[simp]
theorem simple_graph.path.nodup_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.path u v) :
theorem simple_graph.path.loop_eq {V : Type u} {G : simple_graph V} {v : V} (p : G.path v v) :
theorem simple_graph.path.not_mem_edges_of_loop {V : Type u} {G : simple_graph V} {v : V} {e : sym2 V} {p : G.path v v} :
theorem simple_graph.path.cons_is_cycle {V : Type u} {G : simple_graph V} {u v : V} (p : G.path v u) (h : G.adj u v) (he : (u, v) p.edges) :

### Walks to paths #

def simple_graph.walk.bypass {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} :
G.walk u v G.walk u v

Given a walk, produces a walk from it by bypassing subwalks between repeated vertices. The result is a path, as shown in `simple_graph.walk.bypass_is_path`. This is packaged up in `simple_graph.walk.to_path`.

Equations
@[simp]
theorem simple_graph.walk.bypass_copy {V : Type u} {G : simple_graph V} [decidable_eq V] {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).bypass = p.bypass.copy hu hv
theorem simple_graph.walk.bypass_is_path {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.length_bypass_le {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
def simple_graph.walk.to_path {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
G.path u v

Given a walk, produces a path with the same endpoints using `simple_graph.walk.bypass`.

Equations
theorem simple_graph.walk.support_bypass_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.support_to_path_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.darts_bypass_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.edges_bypass_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.darts_to_path_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.edges_to_path_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :

### Mapping paths #

@[protected]
def simple_graph.walk.map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} :
G.walk u v G'.walk (f u) (f v)

Given a graph homomorphism, map walks to walks.

Equations
@[simp]
theorem simple_graph.walk.map_nil {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u : V} :
@[simp]
theorem simple_graph.walk.map_cons {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) {w : V} (h : G.adj w u) :
@[simp]
theorem simple_graph.walk.map_copy {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv) = .copy _ _
@[simp]
theorem simple_graph.walk.map_id {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.map_map {V : Type u} {V' : Type v} {V'' : Type w} {G : simple_graph V} {G' : simple_graph V'} {G'' : simple_graph V''} (f : G →g G') (f' : G' →g G'') {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.map_eq_of_eq {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {u v : V} (p : G.walk u v) {f : G →g G'} (f' : G →g G') (h : f = f') :
= p).copy _ _

Unlike categories, for graphs vertex equality is an important notion, so needing to be able to to work with equality of graph homomorphisms is a necessary evil.

@[simp]
theorem simple_graph.walk.map_eq_nil_iff {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u : V} {p : G.walk u u} :
@[simp]
theorem simple_graph.walk.length_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.map_append {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v w : V} (p : G.walk u v) (q : G.walk v w) :
(p.append q) = .append
@[simp]
theorem simple_graph.walk.reverse_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.support_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.darts_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.edges_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
theorem simple_graph.walk.map_is_path_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u v : V} {p : G.walk u v} (hinj : function.injective f) (hp : p.is_path) :
@[protected]
theorem simple_graph.walk.is_path.of_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {u v : V} {p : G.walk u v} {f : G →g G'} (hp : .is_path) :
theorem simple_graph.walk.map_is_path_iff_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u v : V} {p : G.walk u v} (hinj : function.injective f) :
theorem simple_graph.walk.map_is_trail_iff_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u v : V} {p : G.walk u v} (hinj : function.injective f) :
theorem simple_graph.walk.map_is_trail_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u v : V} {p : G.walk u v} (hinj : function.injective f) :

Alias of the reverse direction of `simple_graph.walk.map_is_trail_iff_of_injective`.

theorem simple_graph.walk.map_is_cycle_iff_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u : V} {p : G.walk u u} (hinj : function.injective f) :
theorem simple_graph.walk.map_is_cycle_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u : V} {p : G.walk u u} (hinj : function.injective f) :

Alias of the reverse direction of `simple_graph.walk.map_is_cycle_iff_of_injective`.

theorem simple_graph.walk.map_injective_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} (hinj : function.injective f) (u v : V) :
@[reducible]
def simple_graph.walk.map_le {V : Type u} {G G' : simple_graph V} (h : G G') {u v : V} (p : G.walk u v) :
G'.walk u v

The specialization of `simple_graph.walk.map` for mapping walks to supergraphs.

Equations
@[simp]
theorem simple_graph.walk.map_le_is_trail {V : Type u} {G G' : simple_graph V} (h : G G') {u v : V} {p : G.walk u v} :
theorem simple_graph.walk.is_trail.map_le {V : Type u} {G G' : simple_graph V} (h : G G') {u v : V} {p : G.walk u v} :

Alias of the reverse direction of `simple_graph.walk.map_le_is_trail`.

theorem simple_graph.walk.is_trail.of_map_le {V : Type u} {G G' : simple_graph V} (h : G G') {u v : V} {p : G.walk u v} :

Alias of the forward direction of `simple_graph.walk.map_le_is_trail`.

@[simp]
theorem simple_graph.walk.map_le_is_path {V : Type u} {G G' : simple_graph V} (h : G G') {u v : V} {p : G.walk u v} :
theorem simple_graph.walk.is_path.of_map_le {V : Type u} {G G' : simple_graph V} (h : G G') {u v : V} {p : G.walk u v} :

Alias of the forward direction of `simple_graph.walk.map_le_is_path`.

theorem simple_graph.walk.is_path.map_le {V : Type u} {G G' : simple_graph V} (h : G G') {u v : V} {p : G.walk u v} :

Alias of the reverse direction of `simple_graph.walk.map_le_is_path`.

@[simp]
theorem simple_graph.walk.map_le_is_cycle {V : Type u} {G G' : simple_graph V} (h : G G') {u : V} {p : G.walk u u} :
theorem simple_graph.walk.is_cycle.of_map_le {V : Type u} {G G' : simple_graph V} (h : G G') {u : V} {p : G.walk u u} :

Alias of the forward direction of `simple_graph.walk.map_le_is_cycle`.

theorem simple_graph.walk.is_cycle.map_le {V : Type u} {G G' : simple_graph V} (h : G G') {u : V} {p : G.walk u u} :

Alias of the reverse direction of `simple_graph.walk.map_le_is_cycle`.

@[simp]
theorem simple_graph.path.map_coe {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') (hinj : function.injective f) {u v : V} (p : G.path u v) :
hinj p) =
@[protected]
def simple_graph.path.map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') (hinj : function.injective f) {u v : V} (p : G.path u v) :
G'.path (f u) (f v)

Given an injective graph homomorphism, map paths to paths.

Equations
• hinj p = , _⟩
theorem simple_graph.path.map_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} (hinj : function.injective f) (u v : V) :
@[protected]
def simple_graph.path.map_embedding {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G ↪g G') {u v : V} (p : G.path u v) :
G'.path (f u) (f v)

Given a graph embedding, map paths to paths.

Equations
@[simp]
theorem simple_graph.path.map_embedding_coe {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G ↪g G') {u v : V} (p : G.path u v) :
theorem simple_graph.path.map_embedding_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G ↪g G') (u v : V) :

### Transferring between graphs #

@[protected, simp]
def simple_graph.walk.transfer {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) (H : simple_graph V) (h : (e : sym2 V), e p.edges ) :
H.walk u v

The walk `p` transferred to lie in `H`, given that `H` contains its edges.

Equations
theorem simple_graph.walk.transfer_self {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.transfer G _ = p
theorem simple_graph.walk.transfer_eq_map_of_le {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {H : simple_graph V} (hp : (e : sym2 V), e p.edges ) (GH : G H) :
@[simp]
theorem simple_graph.walk.edges_transfer {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {H : simple_graph V} (hp : (e : sym2 V), e p.edges ) :
(p.transfer H hp).edges = p.edges
@[simp]
theorem simple_graph.walk.support_transfer {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {H : simple_graph V} (hp : (e : sym2 V), e p.edges ) :
@[simp]
theorem simple_graph.walk.length_transfer {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {H : simple_graph V} (hp : (e : sym2 V), e p.edges ) :
(p.transfer H hp).length = p.length
@[protected]
theorem simple_graph.walk.is_path.transfer {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} {H : simple_graph V} (hp : (e : sym2 V), e p.edges ) (pp : p.is_path) :
(p.transfer H hp).is_path
@[protected]
theorem simple_graph.walk.is_cycle.transfer {V : Type u} {G : simple_graph V} {u : V} {H : simple_graph V} {p : G.walk u u} (pc : p.is_cycle) (hp : (e : sym2 V), e p.edges ) :
@[simp]
theorem simple_graph.walk.transfer_transfer {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {H : simple_graph V} (hp : (e : sym2 V), e p.edges ) {K : simple_graph V} (hp' : (e : sym2 V), e p.edges ) :
(p.transfer H hp).transfer K _ = p.transfer K hp'
@[simp]
theorem simple_graph.walk.transfer_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) {H : simple_graph V} (hpq : (e : sym2 V), e (p.append q).edges ) :
(p.append q).transfer H hpq = (p.transfer H _).append (q.transfer H _)
@[simp]
theorem simple_graph.walk.reverse_transfer {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {H : simple_graph V} (hp : (e : sym2 V), e p.edges ) :

## Deleting edges #

@[reducible]
def simple_graph.walk.to_delete_edges {V : Type u} {G : simple_graph V} (s : set (sym2 V)) {v w : V} (p : G.walk v w) (hp : (e : sym2 V), e p.edges e s) :
(G.delete_edges s).walk v w

Given a walk that avoids a set of edges, produce a walk in the graph with those edges deleted.

Equations
@[simp]
theorem simple_graph.walk.to_delete_edges_nil {V : Type u} {G : simple_graph V} (s : set (sym2 V)) {v : V} (hp : (e : sym2 V), e s) :
@[simp]
theorem simple_graph.walk.to_delete_edges_cons {V : Type u} {G : simple_graph V} (s : set (sym2 V)) {u v w : V} (h : G.adj u v) (p : G.walk v w) (hp : (e : sym2 V), e .edges e s) :
@[reducible]
def simple_graph.walk.to_delete_edge {V : Type u} {G : simple_graph V} {v w : V} (e : sym2 V) (p : G.walk v w) (hp : e p.edges) :
(G.delete_edges {e}).walk v w

Given a walk that avoids an edge, create a walk in the subgraph with that edge deleted. This is an abbreviation for `simple_graph.walk.to_delete_edges`.

@[simp]
theorem simple_graph.walk.map_to_delete_edges_eq {V : Type u} {G : simple_graph V} (s : set (sym2 V)) {v w : V} {p : G.walk v w} (hp : (e : sym2 V), e p.edges e s) :
@[protected]
theorem simple_graph.walk.is_path.to_delete_edges {V : Type u} {G : simple_graph V} (s : set (sym2 V)) {v w : V} {p : G.walk v w} (h : p.is_path) (hp : (e : sym2 V), e p.edges e s) :
@[protected]
theorem simple_graph.walk.is_cycle.to_delete_edges {V : Type u} {G : simple_graph V} (s : set (sym2 V)) {v : V} {p : G.walk v v} (h : p.is_cycle) (hp : (e : sym2 V), e p.edges e s) :
@[simp]
theorem simple_graph.walk.to_delete_edges_copy {V : Type u} {G : simple_graph V} (s : set (sym2 V)) {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') (h : (e : sym2 V), e (p.copy hu hv).edges e s) :
(p.copy hu hv) h = hu hv

## `reachable` and `connected`#

def simple_graph.reachable {V : Type u} (G : simple_graph V) (u v : V) :
Prop

Two vertices are reachable if there is a walk between them. This is equivalent to `relation.refl_trans_gen` of `G.adj`. See `simple_graph.reachable_iff_refl_trans_gen`.

Equations
Instances for `simple_graph.reachable`
@[protected]
theorem simple_graph.reachable.elim {V : Type u} {G : simple_graph V} {p : Prop} {u v : V} (h : G.reachable u v) (hp : G.walk u v p) :
p
@[protected]
theorem simple_graph.reachable.elim_path {V : Type u} {G : simple_graph V} {p : Prop} {u v : V} (h : G.reachable u v) (hp : G.path u v p) :
p
@[protected]
theorem simple_graph.walk.reachable {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
G.reachable u v
@[protected]
theorem simple_graph.adj.reachable {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
G.reachable u v
@[protected, refl]
theorem simple_graph.reachable.refl {V : Type u} {G : simple_graph V} (u : V) :
G.reachable u u
@[protected]
theorem simple_graph.reachable.rfl {V : Type u} {G : simple_graph V} {u : V} :
G.reachable u u
@[protected, symm]
theorem simple_graph.reachable.symm {V : Type u} {G : simple_graph V} {u v : V} (huv : G.reachable u v) :
G.reachable v u
theorem simple_graph.reachable_comm {V : Type u} {G : simple_graph V} {u v : V} :
G.reachable u v G.reachable v u
@[protected, trans]
theorem simple_graph.reachable.trans {V : Type u} {G : simple_graph V} {u v w : V} (huv : G.reachable u v) (hvw : G.reachable v w) :
G.reachable u w
theorem simple_graph.reachable_iff_refl_trans_gen {V : Type u} {G : simple_graph V} (u v : V) :
G.reachable u v
@[protected]
theorem simple_graph.reachable.map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (h : G.reachable u v) :
G'.reachable (f u) (f v)
theorem simple_graph.iso.reachable_iff {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {φ : G ≃g G'} {u v : V} :
G'.reachable (φ u) (φ v) G.reachable u v
theorem simple_graph.iso.symm_apply_reachable {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {φ : G ≃g G'} {u : V} {v : V'} :
G.reachable ((φ.symm) v) u G'.reachable v (φ u)

The equivalence relation on vertices given by `simple_graph.reachable`.

Equations
def simple_graph.preconnected {V : Type u} (G : simple_graph V) :
Prop

A graph is preconnected if every pair of vertices is reachable from one another.

Equations
Instances for `simple_graph.preconnected`
theorem simple_graph.preconnected.map {V : Type u} {V' : Type v} {G : simple_graph V} {H : simple_graph V'} (f : G →g H) (hf : function.surjective f) (hG : G.preconnected) :
theorem simple_graph.iso.preconnected_iff {V : Type u} {V' : Type v} {G : simple_graph V} {H : simple_graph V'} (e : G ≃g H) :
structure simple_graph.connected {V : Type u} (G : simple_graph V) :
Prop
• preconnected :
• nonempty :

A graph is connected if it's preconnected and contains at least one vertex. This follows the convention observed by mathlib that something is connected iff it has exactly one connected component.

There is a `has_coe_to_fun` instance so that `h u v` can be used instead of `h.preconnected u v`.

Instances for `simple_graph.connected`
@[protected, instance]
def simple_graph.connected.has_coe_to_fun {V : Type u} (G : simple_graph V) :
(λ (_x : G.connected), (u v : V), G.reachable u v)
Equations
theorem simple_graph.connected.map {V : Type u} {V' : Type v} {G : simple_graph V} {H : simple_graph V'} (f : G →g H) (hf : function.surjective f) (hG : G.connected) :
theorem simple_graph.iso.connected_iff {V : Type u} {V' : Type v} {G : simple_graph V} {H : simple_graph V'} (e : G ≃g H) :

The quotient of `V` by the `simple_graph.reachable` relation gives the connected components of a graph.

Equations
Instances for `simple_graph.connected_component`
def simple_graph.connected_component_mk {V : Type u} (G : simple_graph V) (v : V) :

Gives the connected component containing a particular vertex.

Equations
@[protected, instance]
Equations
@[protected]
theorem simple_graph.connected_component.ind {V : Type u} {G : simple_graph V} {β : G.connected_component Prop} (h : (v : V), β ) (c : G.connected_component) :
β c
@[protected]
theorem simple_graph.connected_component.ind₂ {V : Type u} {G : simple_graph V} {β : G.connected_component G.connected_component Prop} (h : (v w : V), β ) (c d : G.connected_component) :
β c d
@[protected]
theorem simple_graph.connected_component.sound {V : Type u} {G : simple_graph V} {v w : V} :
G.reachable v w
@[protected]
theorem simple_graph.connected_component.exact {V : Type u} {G : simple_graph V} {v w : V} :
G.reachable v w
@[protected, simp]
theorem simple_graph.connected_component.eq {V : Type u} {G : simple_graph V} {v w : V} :
G.reachable v w
@[protected]
def simple_graph.connected_component.lift {V : Type u} {G : simple_graph V} {β : Sort u_1} (f : V β) (h : (v w : V) (p : G.walk v w), p.is_path f v = f w) :

The `connected_component` specialization of `quot.lift`. Provides the stronger assumption that the vertices are connected by a path.

Equations
• = quot.lift f _
@[protected, simp]
theorem simple_graph.connected_component.lift_mk {V : Type u} {G : simple_graph V} {β : Sort u_1} {f : V β} {h : (v w : V) (p : G.walk v w), p.is_path f v = f w} {v : V} :
@[protected]
theorem simple_graph.connected_component.exists {V : Type u} {G : simple_graph V} {p : G.connected_component Prop} :
( (c : G.connected_component), p c) (v : V), p
@[protected]
theorem simple_graph.connected_component.forall {V : Type u} {G : simple_graph V} {p : G.connected_component Prop} :
( (c : G.connected_component), p c) (v : V), p
def simple_graph.connected_component.map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G →g G') (C : G.connected_component) :

The map on connected components induced by a graph homomorphism.

Equations
@[simp]
theorem simple_graph.connected_component.map_mk {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G →g G') (v : V) :
@[simp]
theorem simple_graph.connected_component.map_comp {V : Type u} {V' : Type v} {V'' : Type w} {G : simple_graph V} {G' : simple_graph V'} {G'' : simple_graph V''} (C : G.connected_component) (φ : G →g G') (ψ : G' →g G'') :
@[simp]
theorem simple_graph.connected_component.iso_image_comp_eq_map_iff_eq_comp {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {φ : G ≃g G'} {v : V} {C : G.connected_component} :
@[simp]
theorem simple_graph.connected_component.iso_inv_image_comp_eq_iff_eq_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {φ : G ≃g G'} {v' : V'} {C : G.connected_component} :
@[simp]
theorem simple_graph.iso.connected_component_equiv_apply {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G ≃g G') (C : G.connected_component) :
@[simp]
theorem simple_graph.iso.connected_component_equiv_symm_apply {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G ≃g G') (C : G'.connected_component) :
def simple_graph.iso.connected_component_equiv {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G ≃g G') :

An isomorphism of graphs induces a bijection of connected components.

Equations
@[simp]
@[simp]
theorem simple_graph.iso.connected_component_equiv_symm {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G ≃g G') :
@[simp]
theorem simple_graph.iso.connected_component_equiv_trans {V : Type u} {V' : Type v} {V'' : Type w} {G : simple_graph V} {G' : simple_graph V'} {G'' : simple_graph V''} (φ : G ≃g G') (φ' : G' ≃g G'') :

The set of vertices in a connected component of a graph.

Equations
@[ext]
@[simp]
@[protected, instance]
Equations
@[simp]

The equivalence between connected components, induced by an isomorphism of graphs, itself defines an equivalence on the supports of each connected component.

Equations
@[reducible]
def simple_graph.subgraph.connected {V : Type u} {G : simple_graph V} (H : G.subgraph) :
Prop

A subgraph is connected if it is connected as a simple graph.

@[simp]
theorem simple_graph.subgraph_of_adj_connected {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :
theorem simple_graph.preconnected.set_univ_walk_nonempty {V : Type u} {G : simple_graph V} (hconn : G.preconnected) (u v : V) :
theorem simple_graph.connected.set_univ_walk_nonempty {V : Type u} {G : simple_graph V} (hconn : G.connected) (u v : V) :

### Walks as subgraphs #

@[protected, simp]
def simple_graph.walk.to_subgraph {V : Type u} {G : simple_graph V} {u v : V} :
G.walk u v G.subgraph

The subgraph consisting of the vertices and edges of the walk.

Equations
theorem simple_graph.walk.to_subgraph_cons_nil_eq_subgraph_of_adj {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
theorem simple_graph.walk.mem_verts_to_subgraph {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) :
@[simp]
theorem simple_graph.walk.verts_to_subgraph {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.to_subgraph.verts = {w : V | w p.