Graph connectivity

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 [Chou1994].

Main definitions

• SimpleGraph.Walk (with accompanying pattern definitions SimpleGraph.Walk.nil' and SimpleGraph.Walk.cons')

• SimpleGraph.Walk.IsTrail, SimpleGraph.Walk.IsPath, and SimpleGraph.Walk.IsCycle.

• SimpleGraph.Path

• SimpleGraph.Walk.map and SimpleGraph.Path.map for the induced map on walks, given an (injective) graph homomorphism.

• SimpleGraph.Reachable for the relation of whether there exists a walk between a given pair of vertices

• SimpleGraph.Preconnected and SimpleGraph.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.

• SimpleGraph.ConnectedComponent is the type of connected components of a given graph.

• SimpleGraph.IsBridge for whether an edge is a bridge edge

Main statements

• SimpleGraph.isBridge_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 SimpleGraph.Walk {V : Type u} (G : 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.

• nil: {V : Type u} → {G : SimpleGraph V} → {u : V} → G.Walk u u
• cons: {V : Type u} → {G : SimpleGraph V} → {u v w : V} → G.Adj u v → G.Walk v w → G.Walk u w

instance SimpleGraph.instDecidableEqWalk : {V : Type u_1} → {G : SimpleGraph V} → {a a_1 : V} → [inst : DecidableEq V] → DecidableEq (G.Walk a a_1)

Equations

• SimpleGraph.instDecidableEqWalk = SimpleGraph.decEqWalk✝

@[simp]

theorem SimpleGraph.Walk.instInhabited_default {V : Type u} (G : SimpleGraph V) (v : V) : default = SimpleGraph.Walk.nil

instance SimpleGraph.Walk.instInhabited {V : Type u} (G : SimpleGraph V) (v : V) : Inhabited (G.Walk v v)

Equations

• SimpleGraph.Walk.instInhabited G v = { default := SimpleGraph.Walk.nil }

@[reducible, match_pattern]

def SimpleGraph.Adj.toWalk {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) : G.Walk u v

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

Equations

• h.toWalk = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil

@[reducible, match_pattern, inline]

abbrev SimpleGraph.Walk.nil' {V : Type u} {G : SimpleGraph V} (u : V) : G.Walk u u

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

Equations

• SimpleGraph.Walk.nil' u = SimpleGraph.Walk.nil

@[reducible, match_pattern, inline]

abbrev SimpleGraph.Walk.cons' {V : Type u} {G : SimpleGraph V} (u : V) (v : 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.

Equations

• SimpleGraph.Walk.cons' u v w h p = SimpleGraph.Walk.cons h p

def SimpleGraph.Walk.copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {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 = hu ▸ hv ▸ p

@[simp]

theorem SimpleGraph.Walk.copy_rfl_rfl {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.copy ⋯ ⋯ = p

@[simp]

theorem SimpleGraph.Walk.copy_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} {u'' : V} {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 SimpleGraph.Walk.copy_nil {V : Type u} {G : SimpleGraph V} {u : V} {u' : V} (hu : u = u') : SimpleGraph.Walk.nil.copy hu hu = SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.copy_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {u' : V} {w' : V} (h : G.Adj u v) (p : G.Walk v w) (hu : u = u') (hw : w = w') : (SimpleGraph.Walk.cons h p).copy hu hw = SimpleGraph.Walk.cons ⋯ (p.copy ⋯ hw)

@[simp]

theorem SimpleGraph.Walk.cons_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {v' : V} {w' : V} (h : G.Adj u v) (p : G.Walk v' w') (hv : v' = v) (hw : w' = w) : SimpleGraph.Walk.cons h (p.copy hv hw) = (SimpleGraph.Walk.cons ⋯ p).copy ⋯ hw

theorem SimpleGraph.Walk.exists_eq_cons_of_ne {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (hne : u ≠ v) (p : G.Walk u v) : ∃ (w : V) (h : G.Adj u w) (p' : G.Walk w v), p = SimpleGraph.Walk.cons h p'

def SimpleGraph.Walk.length {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : G.Walk u v → ℕ

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

Equations

• SimpleGraph.Walk.nil.length = 0
• (SimpleGraph.Walk.cons h q).length = q.length.succ

def SimpleGraph.Walk.append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} : G.Walk u v → G.Walk v w → G.Walk u w

The concatenation of two compatible walks.

Equations

• SimpleGraph.Walk.nil.append q = q
• (SimpleGraph.Walk.cons h p).append x = SimpleGraph.Walk.cons h (p.append x)

def SimpleGraph.Walk.concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) : G.Walk u w

The reversed version of SimpleGraph.Walk.cons, concatenating an edge to the end of a walk.

Equations

• p.concat h = p.append (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)

theorem SimpleGraph.Walk.concat_eq_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) : p.concat h = p.append (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil)

def SimpleGraph.Walk.reverseAux {V : Type u} {G : SimpleGraph V} {u : V} {v : 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

• SimpleGraph.Walk.nil.reverseAux x = x
• (SimpleGraph.Walk.cons h p).reverseAux x = p.reverseAux (SimpleGraph.Walk.cons ⋯ x)

def SimpleGraph.Walk.reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) : G.Walk v u

The walk in reverse.

Equations

• w.reverse = w.reverseAux SimpleGraph.Walk.nil

def SimpleGraph.Walk.getVert {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : G.Walk u v → ℕ → V

Get the nth 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

• SimpleGraph.Walk.nil.getVert x = u
• (SimpleGraph.Walk.cons h p).getVert 0 = u
• (SimpleGraph.Walk.cons h q).getVert n.succ = q.getVert n

@[simp]

theorem SimpleGraph.Walk.getVert_zero {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) : w.getVert 0 = u

theorem SimpleGraph.Walk.getVert_of_length_le {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) {i : ℕ} (hi : w.length ≤ i) : w.getVert i = v

@[simp]

theorem SimpleGraph.Walk.getVert_length {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) : w.getVert w.length = v

theorem SimpleGraph.Walk.adj_getVert_succ {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (w : G.Walk u v) {i : ℕ} (hi : i < w.length) : G.Adj (w.getVert i) (w.getVert (i + 1))

@[simp]

theorem SimpleGraph.Walk.cons_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (h : G.Adj u v) (p : G.Walk v w) (q : G.Walk w x) : (SimpleGraph.Walk.cons h p).append q = SimpleGraph.Walk.cons h (p.append q)

@[simp]

theorem SimpleGraph.Walk.cons_nil_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).append p = SimpleGraph.Walk.cons h p

@[simp]

theorem SimpleGraph.Walk.append_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.append SimpleGraph.Walk.nil = p

@[simp]

theorem SimpleGraph.Walk.nil_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : SimpleGraph.Walk.nil.append p = p

theorem SimpleGraph.Walk.append_assoc {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {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 SimpleGraph.Walk.append_copy_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {u' : V} {v' : 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 SimpleGraph.Walk.concat_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) : SimpleGraph.Walk.nil.concat h = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.concat_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (h : G.Adj u v) (p : G.Walk v w) (h' : G.Adj w x) : (SimpleGraph.Walk.cons h p).concat h' = SimpleGraph.Walk.cons h (p.concat h')

theorem SimpleGraph.Walk.append_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {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 SimpleGraph.Walk.concat_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (h : G.Adj v w) (q : G.Walk w x) : (p.concat h).append q = p.append (SimpleGraph.Walk.cons h q)

theorem SimpleGraph.Walk.exists_cons_eq_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : 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), SimpleGraph.Walk.cons h p = q.concat h'

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

theorem SimpleGraph.Walk.exists_concat_eq_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : 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 = SimpleGraph.Walk.cons h' q

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

@[simp]

theorem SimpleGraph.Walk.reverse_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.reverse = SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.reverse_singleton {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) : (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil).reverse = SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.cons_reverseAux {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk w x) (h : G.Adj w u) : (SimpleGraph.Walk.cons h p).reverseAux q = p.reverseAux (SimpleGraph.Walk.cons ⋯ q)

@[simp]

theorem SimpleGraph.Walk.append_reverseAux {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk v w) (r : G.Walk u x) : (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)

@[simp]

theorem SimpleGraph.Walk.reverseAux_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : G.Walk u v) (q : G.Walk u w) (r : G.Walk w x) : (p.reverseAux q).append r = p.reverseAux (q.append r)

theorem SimpleGraph.Walk.reverseAux_eq_reverse_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk u w) : p.reverseAux q = p.reverse.append q

@[simp]

theorem SimpleGraph.Walk.reverse_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).reverse = p.reverse.append (SimpleGraph.Walk.cons ⋯ SimpleGraph.Walk.nil)

@[simp]

theorem SimpleGraph.Walk.reverse_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {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 SimpleGraph.Walk.reverse_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).reverse = q.reverse.append p.reverse

@[simp]

theorem SimpleGraph.Walk.reverse_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).reverse = SimpleGraph.Walk.cons ⋯ p.reverse

@[simp]

theorem SimpleGraph.Walk.reverse_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.reverse.reverse = p

theorem SimpleGraph.Walk.reverse_surjective {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : Function.Surjective SimpleGraph.Walk.reverse

theorem SimpleGraph.Walk.reverse_injective {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : Function.Injective SimpleGraph.Walk.reverse

theorem SimpleGraph.Walk.reverse_bijective {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : Function.Bijective SimpleGraph.Walk.reverse

@[simp]

theorem SimpleGraph.Walk.length_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.length = 0

@[simp]

theorem SimpleGraph.Walk.length_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).length = p.length + 1

@[simp]

theorem SimpleGraph.Walk.length_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).length = p.length

@[simp]

theorem SimpleGraph.Walk.length_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).length = p.length + q.length

@[simp]

theorem SimpleGraph.Walk.length_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).length = p.length + 1

@[simp]

theorem SimpleGraph.Walk.length_reverseAux {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk u w) : (p.reverseAux q).length = p.length + q.length

@[simp]

theorem SimpleGraph.Walk.length_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.reverse.length = p.length

theorem SimpleGraph.Walk.eq_of_length_eq_zero {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} : p.length = 0 → u = v

theorem SimpleGraph.Walk.adj_of_length_eq_one {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} : p.length = 1 → G.Adj u v

@[simp]

theorem SimpleGraph.Walk.exists_length_eq_zero_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : (∃ (p : G.Walk u v), p.length = 0) ↔ u = v

@[simp]

theorem SimpleGraph.Walk.length_eq_zero_iff {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.length = 0 ↔ p = SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.getVert_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) (i : ℕ) : (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)

theorem SimpleGraph.Walk.getVert_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (i : ℕ) : p.reverse.getVert i = p.getVert (p.length - i)

def SimpleGraph.Walk.concatRecAux {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1} (Hnil : {u : V} → motive u u SimpleGraph.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 : V} (p : G.Walk u v) : motive v u p.reverse

Auxiliary definition for SimpleGraph.Walk.concatRec

Equations

• SimpleGraph.Walk.concatRecAux Hnil Hconcat SimpleGraph.Walk.nil = Hnil
• SimpleGraph.Walk.concatRecAux Hnil Hconcat (SimpleGraph.Walk.cons h q) = ⋯ ▸ Hconcat q.reverse ⋯ (SimpleGraph.Walk.concatRecAux Hnil Hconcat q)

def SimpleGraph.Walk.concatRec {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1} (Hnil : {u : V} → motive u u SimpleGraph.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 : V} (p : G.Walk u v) : motive u v p

Recursor on walks by inducting on SimpleGraph.Walk.concat.

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

Equations

• SimpleGraph.Walk.concatRec Hnil Hconcat p = ⋯ ▸ SimpleGraph.Walk.concatRecAux Hnil Hconcat p.reverse

@[simp]

theorem SimpleGraph.Walk.concatRec_nil {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1} (Hnil : {u : V} → motive u u SimpleGraph.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) : SimpleGraph.Walk.concatRec Hnil Hconcat SimpleGraph.Walk.nil = Hnil

@[simp]

theorem SimpleGraph.Walk.concatRec_concat {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → G.Walk u v → Sort u_1} (Hnil : {u : V} → motive u u SimpleGraph.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 : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) : SimpleGraph.Walk.concatRec Hnil Hconcat (p.concat h) = Hconcat p h (SimpleGraph.Walk.concatRec Hnil Hconcat p)

theorem SimpleGraph.Walk.concat_ne_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (h : G.Adj v u) : p.concat h ≠ SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.concat_inj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {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 ⋯ hv = p'

def SimpleGraph.Walk.support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : G.Walk u v → List V

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

Equations

• SimpleGraph.Walk.nil.support = [u]
• (SimpleGraph.Walk.cons h q).support = u :: q.support

def SimpleGraph.Walk.darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : G.Walk u v → List G.Dart

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

Equations

• SimpleGraph.Walk.nil.darts = []
• (SimpleGraph.Walk.cons h q).darts = { toProd := (u, v_3), adj := h } :: q.darts

def SimpleGraph.Walk.edges {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : List (Sym2 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 SimpleGraph.Walk.darts.

Equations

• p.edges = List.map SimpleGraph.Dart.edge p.darts

@[simp]

theorem SimpleGraph.Walk.support_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.support = [u]

@[simp]

theorem SimpleGraph.Walk.support_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).support = u :: p.support

@[simp]

theorem SimpleGraph.Walk.support_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).support = p.support.concat w

@[simp]

theorem SimpleGraph.Walk.support_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).support = p.support

theorem SimpleGraph.Walk.support_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) : (p.append p').support = p.support ++ p'.support.tail

@[simp]

theorem SimpleGraph.Walk.support_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.reverse.support = p.support.reverse

@[simp]

theorem SimpleGraph.Walk.support_ne_nil {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.support ≠ []

theorem SimpleGraph.Walk.tail_support_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) : (p.append p').support.tail = p.support.tail ++ p'.support.tail

theorem SimpleGraph.Walk.support_eq_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.support = u :: p.support.tail

@[simp]

theorem SimpleGraph.Walk.start_mem_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : u ∈ p.support

@[simp]

theorem SimpleGraph.Walk.end_mem_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : v ∈ p.support

@[simp]

theorem SimpleGraph.Walk.support_nonempty {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : {w : V | w ∈ p.support}.Nonempty

theorem SimpleGraph.Walk.mem_support_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) : w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail

theorem SimpleGraph.Walk.mem_support_nil_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : u ∈ SimpleGraph.Walk.nil.support ↔ u = v

@[simp]

theorem SimpleGraph.Walk.mem_tail_support_append_iff {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) : t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail

@[simp]

theorem SimpleGraph.Walk.end_mem_tail_support_of_ne {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : u ≠ v) (p : G.Walk u v) : v ∈ p.support.tail

@[simp]

theorem SimpleGraph.Walk.mem_support_append_iff {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) : t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support

@[simp]

theorem SimpleGraph.Walk.subset_support_append_left {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) : p.support ⊆ (p.append q).support

@[simp]

theorem SimpleGraph.Walk.subset_support_append_right {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) : q.support ⊆ (p.append q).support

theorem SimpleGraph.Walk.coe_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : ↑p.support = {u} + ↑p.support.tail

theorem SimpleGraph.Walk.coe_support_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) : ↑(p.append p').support = {u} + ↑p.support.tail + ↑p'.support.tail

theorem SimpleGraph.Walk.coe_support_append' {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) : ↑(p.append p').support = ↑p.support + ↑p'.support - {v}

theorem SimpleGraph.Walk.chain_adj_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) : List.Chain G.Adj u p.support

theorem SimpleGraph.Walk.chain'_adj_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : List.Chain' G.Adj p.support

theorem SimpleGraph.Walk.chain_dartAdj_darts {V : Type u} {G : SimpleGraph V} {d : G.Dart} {v : V} {w : V} (h : d.toProd.2 = v) (p : G.Walk v w) : List.Chain G.DartAdj d p.darts

theorem SimpleGraph.Walk.chain'_dartAdj_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : List.Chain' G.DartAdj p.darts

theorem SimpleGraph.Walk.edges_subset_edgeSet {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) ⦃e : Sym2 V⦄ : e ∈ p.edges → e ∈ G.edgeSet

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 SimpleGraph.Walk.adj_of_mem_edges {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {x : V} {y : V} (p : G.Walk u v) (h : s(x, y) ∈ p.edges) : G.Adj x y

@[simp]

theorem SimpleGraph.Walk.darts_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.darts = []

@[simp]

theorem SimpleGraph.Walk.darts_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).darts = { toProd := (u, v), adj := h } :: p.darts

@[simp]

theorem SimpleGraph.Walk.darts_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).darts = p.darts.concat { toProd := (v, w), adj := h }

@[simp]

theorem SimpleGraph.Walk.darts_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).darts = p.darts

@[simp]

theorem SimpleGraph.Walk.darts_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) : (p.append p').darts = p.darts ++ p'.darts

@[simp]

theorem SimpleGraph.Walk.darts_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.reverse.darts = (List.map SimpleGraph.Dart.symm p.darts).reverse

theorem SimpleGraph.Walk.mem_darts_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {d : G.Dart} {p : G.Walk u v} : d ∈ p.reverse.darts ↔ d.symm ∈ p.darts

theorem SimpleGraph.Walk.cons_map_snd_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : u :: List.map (fun (x : G.Dart) => x.toProd.2) p.darts = p.support

theorem SimpleGraph.Walk.map_snd_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : List.map (fun (x : G.Dart) => x.toProd.2) p.darts = p.support.tail

theorem SimpleGraph.Walk.map_fst_darts_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : List.map (fun (x : G.Dart) => x.toProd.1) p.darts ++ [v] = p.support

theorem SimpleGraph.Walk.map_fst_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : List.map (fun (x : G.Dart) => x.toProd.1) p.darts = p.support.dropLast

@[simp]

theorem SimpleGraph.Walk.edges_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.edges = []

@[simp]

theorem SimpleGraph.Walk.edges_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).edges = s(u, v) :: p.edges

@[simp]

theorem SimpleGraph.Walk.edges_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (h : G.Adj v w) : (p.concat h).edges = p.edges.concat s(v, w)

@[simp]

theorem SimpleGraph.Walk.edges_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).edges = p.edges

@[simp]

theorem SimpleGraph.Walk.edges_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : G.Walk u v) (p' : G.Walk v w) : (p.append p').edges = p.edges ++ p'.edges

@[simp]

theorem SimpleGraph.Walk.edges_reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.reverse.edges = p.edges.reverse

@[simp]

theorem SimpleGraph.Walk.length_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.support.length = p.length + 1

@[simp]

theorem SimpleGraph.Walk.length_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.darts.length = p.length

@[simp]

theorem SimpleGraph.Walk.length_edges {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.edges.length = p.length

theorem SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {d : G.Dart} : d ∈ p.darts → d.toProd.1 ∈ p.support

theorem SimpleGraph.Walk.dart_snd_mem_support_of_mem_darts {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {d : G.Dart} (h : d ∈ p.darts) : d.toProd.2 ∈ p.support

theorem SimpleGraph.Walk.fst_mem_support_of_mem_edges {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : G.Walk v w) (he : s(t, u) ∈ p.edges) : t ∈ p.support

theorem SimpleGraph.Walk.snd_mem_support_of_mem_edges {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : G.Walk v w) (he : s(t, u) ∈ p.edges) : u ∈ p.support

theorem SimpleGraph.Walk.darts_nodup_of_support_nodup {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.darts.Nodup

theorem SimpleGraph.Walk.edges_nodup_of_support_nodup {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.edges.Nodup

inductive SimpleGraph.Walk.Nil {V : Type u} {G : SimpleGraph V} {v : V} {w : V} : G.Walk v w → Prop

Predicate for the empty walk.

Solves the dependent type problem where p = G.Walk.nil typechecks only if p has defeq endpoints.

• nil: ∀ {V : Type u} {G : SimpleGraph V} {u : V}, SimpleGraph.Walk.nil.Nil

@[simp]

theorem SimpleGraph.Walk.nil_nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.Nil

@[simp]

theorem SimpleGraph.Walk.not_nil_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {h : G.Adj u v} {p : G.Walk v w} : ¬(SimpleGraph.Walk.cons h p).Nil

instance SimpleGraph.Walk.instDecidableNil {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) : Decidable p.Nil

Equations

• p.instDecidableNil = match w, p with | .(v), SimpleGraph.Walk.nil => isTrue ⋯ | w, SimpleGraph.Walk.cons h p => isFalse ⋯

theorem SimpleGraph.Walk.Nil.eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} : p.Nil → v = w

theorem SimpleGraph.Walk.not_nil_of_ne {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} : v ≠ w → ¬p.Nil

theorem SimpleGraph.Walk.nil_iff_support_eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} : p.Nil ↔ p.support = [v]

theorem SimpleGraph.Walk.nil_iff_length_eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} : p.Nil ↔ p.length = 0

theorem SimpleGraph.Walk.not_nil_iff {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} : ¬p.Nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w), p = SimpleGraph.Walk.cons h q

theorem SimpleGraph.Walk.nil_iff_eq_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} : p.Nil ↔ p = SimpleGraph.Walk.nil

A walk with its endpoints defeq is Nil if and only if it is equal to nil.

theorem SimpleGraph.Walk.Nil.eq_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} : p.Nil → p = SimpleGraph.Walk.nil

Alias of the forward direction of SimpleGraph.Walk.nil_iff_eq_nil.

---

A walk with its endpoints defeq is Nil if and only if it is equal to nil.

def SimpleGraph.Walk.notNilRec {V : Type u} {G : SimpleGraph V} {u : V} {w : V} {motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1} (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (SimpleGraph.Walk.cons h q) ⋯) (p : G.Walk u w) (hp : ¬p.Nil) : motive p hp

Equations

• One or more equations did not get rendered due to their size.

def SimpleGraph.Walk.sndOfNotNil {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) : V

The second vertex along a non-nil walk.

Equations

• p.sndOfNotNil hp = SimpleGraph.Walk.notNilRec (fun (x u x_1 : V) (x : G.Adj x u) (x : G.Walk u x_1) => u) p hp

@[simp]

theorem SimpleGraph.Walk.adj_sndOfNotNil {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {p : G.Walk v w} (hp : ¬p.Nil) : G.Adj v (p.sndOfNotNil hp)

def SimpleGraph.Walk.tail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (hp : ¬p.Nil) : G.Walk (p.sndOfNotNil hp) v

The walk obtained by removing the first dart of a non-nil walk.

Equations

• p.tail hp = SimpleGraph.Walk.notNilRec (fun {u v w : V} (x : G.Adj u v) (q : G.Walk v w) => q) p hp

@[simp]

theorem SimpleGraph.Walk.firstDart_toProd {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.firstDart hp).toProd = (v, p.sndOfNotNil hp)

def SimpleGraph.Walk.firstDart {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) : G.Dart

The first dart of a walk.

Equations

• p.firstDart hp = { toProd := (v, p.sndOfNotNil hp), adj := ⋯ }

theorem SimpleGraph.Walk.edge_firstDart {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : G.Walk v w) (hp : ¬p.Nil) : (p.firstDart hp).edge = s(v, p.sndOfNotNil hp)

@[simp]

theorem SimpleGraph.Walk.cons_tail_eq {V : Type u} {G : SimpleGraph V} {x : V} {y : V} (p : G.Walk x y) (hp : ¬p.Nil) : SimpleGraph.Walk.cons ⋯ (p.tail hp) = p

@[simp]

theorem SimpleGraph.Walk.cons_support_tail {V : Type u} {G : SimpleGraph V} {x : V} {y : V} (p : G.Walk x y) (hp : ¬p.Nil) : x :: (p.tail hp).support = p.support

@[simp]

theorem SimpleGraph.Walk.length_tail_add_one {V : Type u} {G : SimpleGraph V} {x : V} {y : V} {p : G.Walk x y} (hp : ¬p.Nil) : (p.tail hp).length + 1 = p.length

@[simp]

theorem SimpleGraph.Walk.nil_copy {V : Type u} {G : SimpleGraph V} {x : V} {y : V} {x' : V} {y' : V} {p : G.Walk x y} (hx : x = x') (hy : y = y') : (p.copy hx hy).Nil = p.Nil

@[simp]

theorem SimpleGraph.Walk.support_tail {V : Type u} {G : SimpleGraph V} {v : V} (p : G.Walk v v) (hp : ¬p.Nil) : (p.tail hp).support = p.support.tail

Trails, paths, circuits, cycles

theorem SimpleGraph.Walk.isTrail_def {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.IsTrail ↔ p.edges.Nodup

structure SimpleGraph.Walk.IsTrail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : Prop

A trail is a walk with no repeating edges.

• edges_nodup : p.edges.Nodup

theorem SimpleGraph.Walk.IsTrail.edges_nodup {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (self : p.IsTrail) : p.edges.Nodup

structure SimpleGraph.Walk.IsPath {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) extends SimpleGraph.Walk.IsTrail : Prop

A path is a walk with no repeating vertices. Use SimpleGraph.Walk.IsPath.mk' for a simpler constructor.

• edges_nodup : p.edges.Nodup
• support_nodup : p.support.Nodup

theorem SimpleGraph.Walk.IsPath.support_nodup {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (self : p.IsPath) : p.support.Nodup

theorem SimpleGraph.Walk.IsPath.isTrail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.IsPath) : p.IsTrail

theorem SimpleGraph.Walk.isCircuit_def {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) : p.IsCircuit ↔ p.IsTrail ∧ p ≠ SimpleGraph.Walk.nil

structure SimpleGraph.Walk.IsCircuit {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) extends SimpleGraph.Walk.IsTrail : Prop

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

• edges_nodup : p.edges.Nodup
• ne_nil : p ≠ SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.IsCircuit.ne_nil {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (self : p.IsCircuit) : p ≠ SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.IsCircuit.isTrail {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCircuit) : p.IsTrail

structure SimpleGraph.Walk.IsCycle {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) extends SimpleGraph.Walk.IsCircuit : Prop

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

• edges_nodup : p.edges.Nodup
• ne_nil : p ≠ SimpleGraph.Walk.nil
• support_nodup : p.support.tail.Nodup

theorem SimpleGraph.Walk.IsCycle.support_nodup {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (self : p.IsCycle) : p.support.tail.Nodup

theorem SimpleGraph.Walk.IsCycle.isCircuit {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} (h : p.IsCycle) : p.IsCircuit

@[simp]

theorem SimpleGraph.Walk.isTrail_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).IsTrail ↔ p.IsTrail

theorem SimpleGraph.Walk.IsPath.mk' {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.support.Nodup) : p.IsPath

theorem SimpleGraph.Walk.isPath_def {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.IsPath ↔ p.support.Nodup

@[simp]

theorem SimpleGraph.Walk.isPath_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).IsPath ↔ p.IsPath

@[simp]

theorem SimpleGraph.Walk.isCircuit_copy {V : Type u} {G : SimpleGraph V} {u : V} {u' : V} (p : G.Walk u u) (hu : u = u') : (p.copy hu hu).IsCircuit ↔ p.IsCircuit

theorem SimpleGraph.Walk.IsCircuit.not_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCircuit) : ¬p.Nil

theorem SimpleGraph.Walk.isCycle_def {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) : p.IsCycle ↔ p.IsTrail ∧ p ≠ SimpleGraph.Walk.nil ∧ p.support.tail.Nodup

@[simp]

theorem SimpleGraph.Walk.isCycle_copy {V : Type u} {G : SimpleGraph V} {u : V} {u' : V} (p : G.Walk u u) (hu : u = u') : (p.copy hu hu).IsCycle ↔ p.IsCycle

theorem SimpleGraph.Walk.IsCycle.not_nil {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) : ¬p.Nil

@[simp]

theorem SimpleGraph.Walk.IsTrail.nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.IsTrail

theorem SimpleGraph.Walk.IsTrail.of_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {h : G.Adj u v} {p : G.Walk v w} : (SimpleGraph.Walk.cons h p).IsTrail → p.IsTrail

@[simp]

theorem SimpleGraph.Walk.cons_isTrail_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges

theorem SimpleGraph.Walk.IsTrail.reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (h : p.IsTrail) : p.reverse.IsTrail

@[simp]

theorem SimpleGraph.Walk.reverse_isTrail_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.reverse.IsTrail ↔ p.IsTrail

theorem SimpleGraph.Walk.IsTrail.of_append_left {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) : p.IsTrail

theorem SimpleGraph.Walk.IsTrail.of_append_right {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsTrail) : q.IsTrail

theorem SimpleGraph.Walk.IsTrail.count_edges_le_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : G.Walk u v} (h : p.IsTrail) (e : Sym2 V) : List.count e p.edges ≤ 1

theorem SimpleGraph.Walk.IsTrail.count_edges_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : G.Walk u v} (h : p.IsTrail) {e : Sym2 V} (he : e ∈ p.edges) : List.count e p.edges = 1

theorem SimpleGraph.Walk.IsPath.nil {V : Type u} {G : SimpleGraph V} {u : V} : SimpleGraph.Walk.nil.IsPath

theorem SimpleGraph.Walk.IsPath.of_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {h : G.Adj u v} {p : G.Walk v w} : (SimpleGraph.Walk.cons h p).IsPath → p.IsPath

@[simp]

theorem SimpleGraph.Walk.cons_isPath_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) : (SimpleGraph.Walk.cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support

theorem SimpleGraph.Walk.IsPath.cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk v w} (hp : p.IsPath) (hu : u ∉ p.support) {h : G.Adj u v} : (SimpleGraph.Walk.cons h p).IsPath

@[simp]

theorem SimpleGraph.Walk.isPath_iff_eq_nil {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u) : p.IsPath ↔ p = SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.IsPath.reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (h : p.IsPath) : p.reverse.IsPath

@[simp]

theorem SimpleGraph.Walk.isPath_reverse_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.reverse.IsPath ↔ p.IsPath

theorem SimpleGraph.Walk.IsPath.of_append_left {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} : (p.append q).IsPath → p.IsPath

theorem SimpleGraph.Walk.IsPath.of_append_right {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {p : G.Walk u v} {q : G.Walk v w} (h : (p.append q).IsPath) : q.IsPath

@[simp]

theorem SimpleGraph.Walk.IsCycle.not_of_nil {V : Type u} {G : SimpleGraph V} {u : V} : ¬SimpleGraph.Walk.nil.IsCycle

theorem SimpleGraph.Walk.IsCycle.ne_bot {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u} : p.IsCycle → G ≠ ⊥

theorem SimpleGraph.Walk.IsCycle.three_le_length {V : Type u} {G : SimpleGraph V} {v : V} {p : G.Walk v v} (hp : p.IsCycle) : 3 ≤ p.length

theorem SimpleGraph.Walk.cons_isCycle_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk v u) (h : G.Adj u v) : (SimpleGraph.Walk.cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges

theorem SimpleGraph.Walk.IsPath.tail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} (hp : p.IsPath) (hp' : ¬p.Nil) : (p.tail hp').IsPath

About paths

instance SimpleGraph.Walk.instDecidableIsPathOfDecidableEq {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : Decidable p.IsPath

Equations

• p.instDecidableIsPathOfDecidableEq = ⋯.mpr inferInstance

theorem SimpleGraph.Walk.IsPath.length_lt {V : Type u} {G : SimpleGraph V} [Fintype V] {u : V} {v : V} {p : G.Walk u v} (hp : p.IsPath) : p.length < Fintype.card V

Walk decompositions

def SimpleGraph.Walk.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : V} (p : G.Walk v w) (u : V) : 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

• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.nil.takeUntil x x_1 = ⋯.mpr SimpleGraph.Walk.nil

def SimpleGraph.Walk.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : V} (p : G.Walk v w) (u : V) : 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

• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.nil.dropUntil x x_1 = ⋯.mpr SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.take_spec {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).append (p.dropUntil u h) = p

The takeUntil and dropUntil functions split a walk into two pieces. The lemma SimpleGraph.Walk.count_support_takeUntil_eq_one specifies where this split occurs.

theorem SimpleGraph.Walk.mem_support_iff_exists_append {V : Type u} {G : SimpleGraph V} {u : V} {v : 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 SimpleGraph.Walk.count_support_takeUntil_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : List.count u (p.takeUntil u h).support = 1

theorem SimpleGraph.Walk.count_edges_takeUntil_le_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) (x : V) : List.count s(u, x) (p.takeUntil u h).edges ≤ 1

@[simp]

theorem SimpleGraph.Walk.takeUntil_copy {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {v' : 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).takeUntil u h = (p.takeUntil u ⋯).copy hv ⋯

@[simp]

theorem SimpleGraph.Walk.dropUntil_copy {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {v' : 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).dropUntil u h = (p.dropUntil u ⋯).copy ⋯ hw

theorem SimpleGraph.Walk.support_takeUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).support ⊆ p.support

theorem SimpleGraph.Walk.support_dropUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).support ⊆ p.support

theorem SimpleGraph.Walk.darts_takeUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).darts ⊆ p.darts

theorem SimpleGraph.Walk.darts_dropUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).darts ⊆ p.darts

theorem SimpleGraph.Walk.edges_takeUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).edges ⊆ p.edges

theorem SimpleGraph.Walk.edges_dropUntil_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).edges ⊆ p.edges

theorem SimpleGraph.Walk.length_takeUntil_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.takeUntil u h).length ≤ p.length

theorem SimpleGraph.Walk.length_dropUntil_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : G.Walk v w) (h : u ∈ p.support) : (p.dropUntil u h).length ≤ p.length

theorem SimpleGraph.Walk.IsTrail.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u ∈ p.support) : (p.takeUntil u h).IsTrail

theorem SimpleGraph.Walk.IsTrail.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsTrail) (h : u ∈ p.support) : (p.dropUntil u h).IsTrail

theorem SimpleGraph.Walk.IsPath.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u ∈ p.support) : (p.takeUntil u h).IsPath

theorem SimpleGraph.Walk.IsPath.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Walk v w} (hc : p.IsPath) (h : u ∈ p.support) : (p.dropUntil u h).IsPath

def SimpleGraph.Walk.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {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

• c.rotate h = (c.dropUntil u h).append (c.takeUntil u h)

@[simp]

theorem SimpleGraph.Walk.support_rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).support.tail ~r c.support.tail

theorem SimpleGraph.Walk.rotate_darts {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).darts ~r c.darts

theorem SimpleGraph.Walk.rotate_edges {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (c : G.Walk v v) (h : u ∈ c.support) : (c.rotate h).edges ~r c.edges

theorem SimpleGraph.Walk.IsTrail.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {c : G.Walk v v} (hc : c.IsTrail) (h : u ∈ c.support) : (c.rotate h).IsTrail

theorem SimpleGraph.Walk.IsCircuit.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {c : G.Walk v v} (hc : c.IsCircuit) (h : u ∈ c.support) : (c.rotate h).IsCircuit

theorem SimpleGraph.Walk.IsCycle.rotate {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {c : G.Walk v v} (hc : c.IsCycle) (h : u ∈ c.support) : (c.rotate h).IsCycle

theorem SimpleGraph.Walk.exists_boundary_dart {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (S : Set V) (uS : u ∈ S) (vS : v ∉ S) : ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ 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, inline]

abbrev SimpleGraph.Path {V : Type u} (G : SimpleGraph V) (u : V) (v : V) : Type u

The type for paths between two vertices.

Equations

• G.Path u v = { p : G.Walk u v // p.IsPath }

@[simp]

theorem SimpleGraph.Path.isPath {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) : (↑p).IsPath

@[simp]

theorem SimpleGraph.Path.isTrail {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) : (↑p).IsTrail

@[simp]

theorem SimpleGraph.Path.nil_coe {V : Type u} {G : SimpleGraph V} {u : V} : ↑SimpleGraph.Path.nil = SimpleGraph.Walk.nil

def SimpleGraph.Path.nil {V : Type u} {G : SimpleGraph V} {u : V} : G.Path u u

The length-0 path at a vertex.

Equations

• SimpleGraph.Path.nil = ⟨SimpleGraph.Walk.nil, ⋯⟩

@[simp]

theorem SimpleGraph.Path.singleton_coe {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) : ↑(SimpleGraph.Path.singleton h) = SimpleGraph.Walk.cons h SimpleGraph.Walk.nil

def SimpleGraph.Path.singleton {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) : G.Path u v

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

Equations

• SimpleGraph.Path.singleton h = ⟨SimpleGraph.Walk.cons h SimpleGraph.Walk.nil, ⋯⟩

theorem SimpleGraph.Path.mk'_mem_edges_singleton {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) : s(u, v) ∈ (↑(SimpleGraph.Path.singleton h)).edges

@[simp]

theorem SimpleGraph.Path.reverse_coe {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) : ↑p.reverse = (↑p).reverse

def SimpleGraph.Path.reverse {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) : G.Path v u

The reverse of a path is another path. See also SimpleGraph.Walk.reverse.

Equations

• p.reverse = ⟨(↑p).reverse, ⋯⟩

theorem SimpleGraph.Path.count_support_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} {p : G.Path u v} (hw : w ∈ (↑p).support) : List.count w (↑p).support = 1

theorem SimpleGraph.Path.count_edges_eq_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {p : G.Path u v} (e : Sym2 V) (hw : e ∈ (↑p).edges) : List.count e (↑p).edges = 1

@[simp]

theorem SimpleGraph.Path.nodup_support {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path u v) : (↑p).support.Nodup

theorem SimpleGraph.Path.loop_eq {V : Type u} {G : SimpleGraph V} {v : V} (p : G.Path v v) : p = SimpleGraph.Path.nil

theorem SimpleGraph.Path.not_mem_edges_of_loop {V : Type u} {G : SimpleGraph V} {v : V} {e : Sym2 V} {p : G.Path v v} : e ∉ (↑p).edges

theorem SimpleGraph.Path.cons_isCycle {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Path v u) (h : G.Adj u v) (he : s(u, v) ∉ (↑p).edges) : (SimpleGraph.Walk.cons h ↑p).IsCycle

Walks to paths

def SimpleGraph.Walk.bypass {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {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 SimpleGraph.Walk.bypass_isPath. This is packaged up in SimpleGraph.Walk.toPath.

Equations

• SimpleGraph.Walk.nil.bypass = SimpleGraph.Walk.nil
• (SimpleGraph.Walk.cons h q).bypass = let p' := q.bypass; if hs : u ∈ p'.support then p'.dropUntil u hs else SimpleGraph.Walk.cons h p'

@[simp]

theorem SimpleGraph.Walk.bypass_copy {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : (p.copy hu hv).bypass = p.bypass.copy hu hv

theorem SimpleGraph.Walk.bypass_isPath {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : p.bypass.IsPath

theorem SimpleGraph.Walk.length_bypass_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : p.bypass.length ≤ p.length

theorem SimpleGraph.Walk.bypass_eq_self_of_length_le {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) (h : p.length ≤ p.bypass.length) : p.bypass = p

def SimpleGraph.Walk.toPath {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : G.Path u v

Given a walk, produces a path with the same endpoints using SimpleGraph.Walk.bypass.

Equations

• p.toPath = ⟨p.bypass, ⋯⟩

theorem SimpleGraph.Walk.support_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : p.bypass.support ⊆ p.support

theorem SimpleGraph.Walk.support_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : (↑p.toPath).support ⊆ p.support

theorem SimpleGraph.Walk.darts_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : p.bypass.darts ⊆ p.darts

theorem SimpleGraph.Walk.edges_bypass_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : p.bypass.edges ⊆ p.edges

theorem SimpleGraph.Walk.darts_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : (↑p.toPath).darts ⊆ p.darts

theorem SimpleGraph.Walk.edges_toPath_subset {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} (p : G.Walk u v) : (↑p.toPath).edges ⊆ p.edges

Mapping paths

def SimpleGraph.Walk.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} : G.Walk u v → G'.Walk (f u) (f v)

Given a graph homomorphism, map walks to walks.

Equations

• SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil
• SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h q) = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f q)

@[simp]

theorem SimpleGraph.Walk.map_nil {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} : SimpleGraph.Walk.map f SimpleGraph.Walk.nil = SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.map_cons {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) {w : V} (h : G.Adj w u) : SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.map f p)

@[simp]

theorem SimpleGraph.Walk.map_copy {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} {u' : V} {v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v') : SimpleGraph.Walk.map f (p.copy hu hv) = (SimpleGraph.Walk.map f p).copy ⋯ ⋯

@[simp]

theorem SimpleGraph.Walk.map_id {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (p : G.Walk u v) : SimpleGraph.Walk.map SimpleGraph.Hom.id p = p

@[simp]

theorem SimpleGraph.Walk.map_map {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''} (f : G →g G') (f' : G' →g G'') {u : V} {v : V} (p : G.Walk u v) : SimpleGraph.Walk.map f' (SimpleGraph.Walk.map f p) = SimpleGraph.Walk.map (f'.comp f) p

theorem SimpleGraph.Walk.map_eq_of_eq {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u : V} {v : V} (p : G.Walk u v) {f : G →g G'} (f' : G →g G') (h : f = f') : SimpleGraph.Walk.map f p = (SimpleGraph.Walk.map f' p).copy ⋯ ⋯

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

@[simp]

theorem SimpleGraph.Walk.map_eq_nil_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {p : G.Walk u u} : SimpleGraph.Walk.map f p = SimpleGraph.Walk.nil ↔ p = SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.length_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).length = p.length

theorem SimpleGraph.Walk.map_append {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} {w : V} (p : G.Walk u v) (q : G.Walk v w) : SimpleGraph.Walk.map f (p.append q) = (SimpleGraph.Walk.map f p).append (SimpleGraph.Walk.map f q)

@[simp]

theorem SimpleGraph.Walk.reverse_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).reverse = SimpleGraph.Walk.map f p.reverse

@[simp]

theorem SimpleGraph.Walk.support_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).support = List.map (⇑f) p.support

@[simp]

theorem SimpleGraph.Walk.darts_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).darts = List.map f.mapDart p.darts

@[simp]

theorem SimpleGraph.Walk.edges_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') {u : V} {v : V} (p : G.Walk u v) : (SimpleGraph.Walk.map f p).edges = List.map (Sym2.map ⇑f) p.edges

theorem SimpleGraph.Walk.map_isPath_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) (hp : p.IsPath) : (SimpleGraph.Walk.map f p).IsPath

theorem SimpleGraph.Walk.IsPath.of_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {u : V} {v : V} {p : G.Walk u v} {f : G →g G'} (hp : (SimpleGraph.Walk.map f p).IsPath) : p.IsPath

theorem SimpleGraph.Walk.map_isPath_iff_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : (SimpleGraph.Walk.map f p).IsPath ↔ p.IsPath

theorem SimpleGraph.Walk.map_isTrail_iff_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : (SimpleGraph.Walk.map f p).IsTrail ↔ p.IsTrail

theorem SimpleGraph.Walk.map_isTrail_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {v : V} {p : G.Walk u v} (hinj : Function.Injective ⇑f) : p.IsTrail → (SimpleGraph.Walk.map f p).IsTrail

Alias of the reverse direction of SimpleGraph.Walk.map_isTrail_iff_of_injective.

theorem SimpleGraph.Walk.map_isCycle_iff_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : Function.Injective ⇑f) : (SimpleGraph.Walk.map f p).IsCycle ↔ p.IsCycle

theorem SimpleGraph.Walk.IsCycle.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u : V} {p : G.Walk u u} (hinj : Function.Injective ⇑f) : p.IsCycle → (SimpleGraph.Walk.map f p).IsCycle

Alias of the reverse direction of SimpleGraph.Walk.map_isCycle_iff_of_injective.

theorem SimpleGraph.Walk.map_injective_of_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} (hinj : Function.Injective ⇑f) (u : V) (v : V) : Function.Injective (SimpleGraph.Walk.map f)

@[reducible, inline]

abbrev SimpleGraph.Walk.mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {v : V} (p : G.Walk u v) : G'.Walk u v

The specialization of SimpleGraph.Walk.map for mapping walks to supergraphs.

Equations

• SimpleGraph.Walk.mapLe h p = SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs h) p

@[simp]

theorem SimpleGraph.Walk.mapLe_isTrail {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {v : V} {p : G.Walk u v} : (SimpleGraph.Walk.mapLe h p).IsTrail ↔ p.IsTrail

theorem SimpleGraph.Walk.IsTrail.mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {v : V} {p : G.Walk u v} : p.IsTrail → (SimpleGraph.Walk.mapLe h p).IsTrail

Alias of the reverse direction of SimpleGraph.Walk.mapLe_isTrail.

theorem SimpleGraph.Walk.IsTrail.of_mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {v : V} {p : G.Walk u v} : (SimpleGraph.Walk.mapLe h p).IsTrail → p.IsTrail

Alias of the forward direction of SimpleGraph.Walk.mapLe_isTrail.

@[simp]

theorem SimpleGraph.Walk.mapLe_isPath {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {v : V} {p : G.Walk u v} : (SimpleGraph.Walk.mapLe h p).IsPath ↔ p.IsPath

theorem SimpleGraph.Walk.IsPath.of_mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {v : V} {p : G.Walk u v} : (SimpleGraph.Walk.mapLe h p).IsPath → p.IsPath

Alias of the forward direction of SimpleGraph.Walk.mapLe_isPath.

theorem SimpleGraph.Walk.IsPath.mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {v : V} {p : G.Walk u v} : p.IsPath → (SimpleGraph.Walk.mapLe h p).IsPath

Alias of the reverse direction of SimpleGraph.Walk.mapLe_isPath.

@[simp]

theorem SimpleGraph.Walk.mapLe_isCycle {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u} : (SimpleGraph.Walk.mapLe h p).IsCycle ↔ p.IsCycle

theorem SimpleGraph.Walk.IsCycle.of_mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u} : (SimpleGraph.Walk.mapLe h p).IsCycle → p.IsCycle

Alias of the forward direction of SimpleGraph.Walk.mapLe_isCycle.

theorem SimpleGraph.Walk.IsCycle.mapLe {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u} : p.IsCycle → (SimpleGraph.Walk.mapLe h p).IsCycle

Alias of the reverse direction of SimpleGraph.Walk.mapLe_isCycle.

@[simp]

theorem SimpleGraph.Path.map_coe {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f) {u : V} {v : V} (p : G.Path u v) : ↑(SimpleGraph.Path.map f hinj p) = SimpleGraph.Walk.map f ↑p

def SimpleGraph.Path.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (hinj : Function.Injective ⇑f) {u : V} {v : V} (p : G.Path u v) : G'.Path (f u) (f v)

Given an injective graph homomorphism, map paths to paths.

Equations

• SimpleGraph.Path.map f hinj p = ⟨SimpleGraph.Walk.map f ↑p, ⋯⟩

theorem SimpleGraph.Path.map_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} (hinj : Function.Injective ⇑f) (u : V) (v : V) : Function.Injective (SimpleGraph.Path.map f hinj)

@[simp]

theorem SimpleGraph.Path.mapEmbedding_coe {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u : V} {v : V} (p : G.Path u v) : ↑(SimpleGraph.Path.mapEmbedding f p) = SimpleGraph.Walk.map f.toHom ↑p

def SimpleGraph.Path.mapEmbedding {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') {u : V} {v : V} (p : G.Path u v) : G'.Path (f u) (f v)

Given a graph embedding, map paths to paths.

Equations

• SimpleGraph.Path.mapEmbedding f p = SimpleGraph.Path.map f.toHom ⋯ p

theorem SimpleGraph.Path.mapEmbedding_injective {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ↪g G') (u : V) (v : V) : Function.Injective (SimpleGraph.Path.mapEmbedding f)

### Transferring between graphs

def SimpleGraph.Walk.transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) (H : SimpleGraph V) (h : ∀ e ∈ p.edges, e ∈ H.edgeSet) : H.Walk u v

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

Equations

• SimpleGraph.Walk.nil.transfer H h_2 = SimpleGraph.Walk.nil
• (SimpleGraph.Walk.cons h_2 p_2).transfer H h_3 = SimpleGraph.Walk.cons ⋯ (p_2.transfer H ⋯)

theorem SimpleGraph.Walk.transfer_self {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : p.transfer G ⋯ = p

theorem SimpleGraph.Walk.transfer_eq_map_of_le {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (GH : G ≤ H) : p.transfer H hp = SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs GH) p

@[simp]

theorem SimpleGraph.Walk.edges_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).edges = p.edges

@[simp]

theorem SimpleGraph.Walk.support_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).support = p.support

@[simp]

theorem SimpleGraph.Walk.length_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).length = p.length

theorem SimpleGraph.Walk.IsPath.transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {p : G.Walk u v} {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) (pp : p.IsPath) : (p.transfer H hp).IsPath

theorem SimpleGraph.Walk.IsCycle.transfer {V : Type u} {G : SimpleGraph V} {u : V} {H : SimpleGraph V} {q : G.Walk u u} (qc : q.IsCycle) (hq : ∀ e ∈ q.edges, e ∈ H.edgeSet) : (q.transfer H hq).IsCycle

@[simp]

theorem SimpleGraph.Walk.transfer_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) {K : SimpleGraph V} (hp' : ∀ e ∈ (p.transfer H hp).edges, e ∈ K.edgeSet) : (p.transfer H hp).transfer K hp' = p.transfer K ⋯

@[simp]

theorem SimpleGraph.Walk.transfer_append {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} {w : V} (q : G.Walk v w) (hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet) : (p.append q).transfer H hpq = (p.transfer H ⋯).append (q.transfer H ⋯)

@[simp]

theorem SimpleGraph.Walk.reverse_transfer {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet) : (p.transfer H hp).reverse = p.reverse.transfer H ⋯

Deleting edges

@[reducible, inline]

abbrev SimpleGraph.Walk.toDeleteEdges {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v : V} {w : V} (p : G.Walk v w) (hp : ∀ e ∈ p.edges, e ∉ s) : (G.deleteEdges s).Walk v w

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

Equations

• SimpleGraph.Walk.toDeleteEdges s p hp = p.transfer (G.deleteEdges s) ⋯

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_nil {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v : V} (hp : ∀ e ∈ SimpleGraph.Walk.nil.edges, e ∉ s) : SimpleGraph.Walk.toDeleteEdges s SimpleGraph.Walk.nil hp = SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_cons {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {u : V} {v : V} {w : V} (h : G.Adj u v) (p : G.Walk v w) (hp : ∀ e ∈ (SimpleGraph.Walk.cons h p).edges, e ∉ s) : SimpleGraph.Walk.toDeleteEdges s (SimpleGraph.Walk.cons h p) hp = SimpleGraph.Walk.cons ⋯ (SimpleGraph.Walk.toDeleteEdges s p ⋯)

@[reducible, inline]

abbrev SimpleGraph.Walk.toDeleteEdge {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (e : Sym2 V) (p : G.Walk v w) (hp : e ∉ p.edges) : (G.deleteEdges {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 SimpleGraph.Walk.toDeleteEdges.

Equations

• SimpleGraph.Walk.toDeleteEdge e p hp = SimpleGraph.Walk.toDeleteEdges {e} p ⋯

@[simp]

theorem SimpleGraph.Walk.map_toDeleteEdges_eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (hp : ∀ e ∈ p.edges, e ∉ s) : SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs ⋯) (SimpleGraph.Walk.toDeleteEdges s p hp) = p

theorem SimpleGraph.Walk.IsPath.toDeleteEdges {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (s : Set (Sym2 V)) {p : G.Walk v w} (h : p.IsPath) (hp : ∀ e ∈ p.edges, e ∉ s) : (SimpleGraph.Walk.toDeleteEdges s p hp).IsPath

theorem SimpleGraph.Walk.IsCycle.toDeleteEdges {V : Type u} {G : SimpleGraph V} {v : V} (s : Set (Sym2 V)) {p : G.Walk v v} (h : p.IsCycle) (hp : ∀ e ∈ p.edges, e ∉ s) : (SimpleGraph.Walk.toDeleteEdges s p hp).IsCycle

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_copy {V : Type u} {G : SimpleGraph V} {v : V} {u : V} {u' : V} {v' : V} (s : Set (Sym2 V)) (p : G.Walk u v) (hu : u = u') (hv : v = v') (h : ∀ e ∈ (p.copy hu hv).edges, e ∉ s) : SimpleGraph.Walk.toDeleteEdges s (p.copy hu hv) h = (SimpleGraph.Walk.toDeleteEdges s p ⋯).copy hu hv

Reachable and Connected

def SimpleGraph.Reachable {V : Type u} (G : SimpleGraph V) (u : V) (v : V) : Prop

Two vertices are reachable if there is a walk between them. This is equivalent to Relation.ReflTransGen of G.Adj. See SimpleGraph.reachable_iff_reflTransGen.

Equations

• G.Reachable u v = Nonempty (G.Walk u v)

theorem SimpleGraph.reachable_iff_nonempty_univ {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : G.Reachable u v ↔ Set.univ.Nonempty

theorem SimpleGraph.not_reachable_iff_isEmpty_walk {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : ¬G.Reachable u v ↔ IsEmpty (G.Walk u v)

theorem SimpleGraph.Reachable.elim {V : Type u} {G : SimpleGraph V} {p : Prop} {u : V} {v : V} (h : G.Reachable u v) (hp : G.Walk u v → p) : p

theorem SimpleGraph.Reachable.elim_path {V : Type u} {G : SimpleGraph V} {p : Prop} {u : V} {v : V} (h : G.Reachable u v) (hp : G.Path u v → p) : p

theorem SimpleGraph.Walk.reachable {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : G.Walk u v) : G.Reachable u v

theorem SimpleGraph.Adj.reachable {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : G.Adj u v) : G.Reachable u v

theorem SimpleGraph.Reachable.refl {V : Type u} {G : SimpleGraph V} (u : V) : G.Reachable u u

theorem SimpleGraph.Reachable.rfl {V : Type u} {G : SimpleGraph V} {u : V} : G.Reachable u u

theorem SimpleGraph.Reachable.symm {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (huv : G.Reachable u v) : G.Reachable v u

theorem SimpleGraph.reachable_comm {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : G.Reachable u v ↔ G.Reachable v u

theorem SimpleGraph.Reachable.trans {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (huv : G.Reachable u v) (hvw : G.Reachable v w) : G.Reachable u w

theorem SimpleGraph.reachable_iff_reflTransGen {V : Type u} {G : SimpleGraph V} (u : V) (v : V) : G.Reachable u v ↔ Relation.ReflTransGen G.Adj u v

theorem SimpleGraph.Reachable.map {V : Type u} {V' : Type v} {u : V} {v : V} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G') (h : G.Reachable u v) : G'.Reachable (f u) (f v)

theorem SimpleGraph.Reachable.mono {V : Type u} {u : V} {v : V} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') (Guv : G.Reachable u v) : G'.Reachable u v

theorem SimpleGraph.Iso.reachable_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u : V} {v : V} : G'.Reachable (φ u) (φ v) ↔ G.Reachable u v

theorem SimpleGraph.Iso.symm_apply_reachable {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {u : V} {v : V'} : G.Reachable (φ.symm v) u ↔ G'.Reachable v (φ u)

theorem SimpleGraph.reachable_is_equivalence {V : Type u} (G : SimpleGraph V) : Equivalence G.Reachable

def SimpleGraph.reachableSetoid {V : Type u} (G : SimpleGraph V) : Setoid V

The equivalence relation on vertices given by SimpleGraph.Reachable.

Equations

• G.reachableSetoid = { r := G.Reachable, iseqv := ⋯ }

def SimpleGraph.Preconnected {V : Type u} (G : SimpleGraph V) : Prop

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

Equations

• G.Preconnected = ∀ (u v : V), G.Reachable u v

theorem SimpleGraph.Preconnected.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (f : G →g H) (hf : Function.Surjective ⇑f) (hG : G.Preconnected) : H.Preconnected

theorem SimpleGraph.Preconnected.mono {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') (hG : G.Preconnected) : G'.Preconnected

theorem SimpleGraph.top_preconnected {V : Type u} : ⊤.Preconnected

theorem SimpleGraph.Iso.preconnected_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (e : G ≃g H) : G.Preconnected ↔ H.Preconnected

theorem SimpleGraph.connected_iff {V : Type u} (G : SimpleGraph V) : G.Connected ↔ G.Preconnected ∧ Nonempty V

structure SimpleGraph.Connected {V : Type u} (G : SimpleGraph V) : Prop

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 CoeFun instance so that h u v can be used instead of h.Preconnected u v.

• preconnected : G.Preconnected
• nonempty : Nonempty V

theorem SimpleGraph.Connected.preconnected {V : Type u} {G : SimpleGraph V} (self : G.Connected) : G.Preconnected

theorem SimpleGraph.Connected.nonempty {V : Type u} {G : SimpleGraph V} (self : G.Connected) : Nonempty V

theorem SimpleGraph.connected_iff_exists_forall_reachable {V : Type u} (G : SimpleGraph V) : G.Connected ↔ ∃ (v : V), ∀ (w : V), G.Reachable v w

instance SimpleGraph.instCoeFunConnectedForallForallReachable {V : Type u} (G : SimpleGraph V) : CoeFun G.Connected fun (x : G.Connected) => ∀ (u v : V), G.Reachable u v

Equations

• G.instCoeFunConnectedForallForallReachable = { coe := ⋯ }

theorem SimpleGraph.Connected.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (f : G →g H) (hf : Function.Surjective ⇑f) (hG : G.Connected) : H.Connected

theorem SimpleGraph.Connected.mono {V : Type u} {G : SimpleGraph V} {G' : SimpleGraph V} (h : G ≤ G') (hG : G.Connected) : G'.Connected

theorem SimpleGraph.top_connected {V : Type u} [Nonempty V] : ⊤.Connected

theorem SimpleGraph.Iso.connected_iff {V : Type u} {V' : Type v} {G : SimpleGraph V} {H : SimpleGraph V'} (e : G ≃g H) : G.Connected ↔ H.Connected

def SimpleGraph.ConnectedComponent {V : Type u} (G : SimpleGraph V) : Type u

The quotient of V by the SimpleGraph.Reachable relation gives the connected components of a graph.

Equations

• G.ConnectedComponent = Quot G.Reachable

def SimpleGraph.connectedComponentMk {V : Type u} (G : SimpleGraph V) (v : V) : G.ConnectedComponent

Gives the connected component containing a particular vertex.

Equations

• G.connectedComponentMk v = Quot.mk G.Reachable v

@[simp]

theorem SimpleGraph.ConnectedComponent.inhabited_default {V : Type u} {G : SimpleGraph V} [Inhabited V] : default = G.connectedComponentMk default

instance SimpleGraph.ConnectedComponent.inhabited {V : Type u} {G : SimpleGraph V} [Inhabited V] : Inhabited G.ConnectedComponent

Equations

• SimpleGraph.ConnectedComponent.inhabited = { default := G.connectedComponentMk default }

theorem SimpleGraph.ConnectedComponent.ind {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponent → Prop} (h : ∀ (v : V), β (G.connectedComponentMk v)) (c : G.ConnectedComponent) : β c

theorem SimpleGraph.ConnectedComponent.ind₂ {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponent → G.ConnectedComponent → Prop} (h : ∀ (v w : V), β (G.connectedComponentMk v) (G.connectedComponentMk w)) (c : G.ConnectedComponent) (d : G.ConnectedComponent) : β c d

theorem SimpleGraph.ConnectedComponent.sound {V : Type u} {G : SimpleGraph V} {v : V} {w : V} : G.Reachable v w → G.connectedComponentMk v = G.connectedComponentMk w

theorem SimpleGraph.ConnectedComponent.exact {V : Type u} {G : SimpleGraph V} {v : V} {w : V} : G.connectedComponentMk v = G.connectedComponentMk w → G.Reachable v w

@[simp]

theorem SimpleGraph.ConnectedComponent.eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} : G.connectedComponentMk v = G.connectedComponentMk w ↔ G.Reachable v w

theorem SimpleGraph.ConnectedComponent.connectedComponentMk_eq_of_adj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (a : G.Adj v w) : G.connectedComponentMk v = G.connectedComponentMk w

def SimpleGraph.ConnectedComponent.lift {V : Type u} {G : SimpleGraph V} {β : Sort u_1} (f : V → β) (h : ∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w) : G.ConnectedComponent → β

The ConnectedComponent specialization of Quot.lift. Provides the stronger assumption that the vertices are connected by a path.

Equations

• SimpleGraph.ConnectedComponent.lift f h = Quot.lift f ⋯

@[simp]

theorem SimpleGraph.ConnectedComponent.lift_mk {V : Type u} {G : SimpleGraph V} {β : Sort u_1} {f : V → β} {h : ∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w} {v : V} : SimpleGraph.ConnectedComponent.lift f h (G.connectedComponentMk v) = f v

theorem SimpleGraph.ConnectedComponent.exists {V : Type u} {G : SimpleGraph V} {p : G.ConnectedComponent → Prop} : (∃ (c : G.ConnectedComponent), p c) ↔ ∃ (v : V), p (G.connectedComponentMk v)

theorem SimpleGraph.ConnectedComponent.forall {V : Type u} {G : SimpleGraph V} {p : G.ConnectedComponent → Prop} : (∀ (c : G.ConnectedComponent), p c) ↔ ∀ (v : V), p (G.connectedComponentMk v)

theorem SimpleGraph.Preconnected.subsingleton_connectedComponent {V : Type u} {G : SimpleGraph V} (h : G.Preconnected) : Subsingleton G.ConnectedComponent

def SimpleGraph.ConnectedComponent.recOn {V : Type u} {G : SimpleGraph V} {motive : G.ConnectedComponent → Sort u_1} (c : G.ConnectedComponent) (f : (v : V) → motive (G.connectedComponentMk v)) (h : ∀ (u v : V) (p : G.Walk u v), p.IsPath → ⋯ ▸ f u = f v) : motive c

This is Quot.recOn specialized to connected components. For convenience, it strengthens the assumptions in the hypothesis to provide a path between the vertices.

Equations

• SimpleGraph.ConnectedComponent.recOn c f h = Quot.recOn c f ⋯

def SimpleGraph.ConnectedComponent.map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G →g G') (C : G.ConnectedComponent) : G'.ConnectedComponent

The map on connected components induced by a graph homomorphism.

Equations

• SimpleGraph.ConnectedComponent.map φ C = SimpleGraph.ConnectedComponent.lift (fun (v : V) => G'.connectedComponentMk (φ v)) ⋯ C

@[simp]

theorem SimpleGraph.ConnectedComponent.map_mk {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G →g G') (v : V) : SimpleGraph.ConnectedComponent.map φ (G.connectedComponentMk v) = G'.connectedComponentMk (φ v)

@[simp]

theorem SimpleGraph.ConnectedComponent.map_id {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : SimpleGraph.ConnectedComponent.map SimpleGraph.Hom.id C = C

@[simp]

theorem SimpleGraph.ConnectedComponent.map_comp {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''} (C : G.ConnectedComponent) (φ : G →g G') (ψ : G' →g G'') : SimpleGraph.ConnectedComponent.map ψ (SimpleGraph.ConnectedComponent.map φ C) = SimpleGraph.ConnectedComponent.map (ψ.comp φ) C

@[simp]

theorem SimpleGraph.ConnectedComponent.iso_image_comp_eq_map_iff_eq_comp {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {v : V} {C : G.ConnectedComponent} : G'.connectedComponentMk (φ v) = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C ↔ G.connectedComponentMk v = C

@[simp]

theorem SimpleGraph.ConnectedComponent.iso_inv_image_comp_eq_iff_eq_map {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {φ : G ≃g G'} {v' : V'} {C : G.ConnectedComponent} : G.connectedComponentMk (φ.symm v') = C ↔ G'.connectedComponentMk v' = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_apply {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') (C : G.ConnectedComponent) : φ.connectedComponentEquiv C = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ).toRelHom C

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_symm_apply {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') (C : G'.ConnectedComponent) : φ.connectedComponentEquiv.symm C = SimpleGraph.ConnectedComponent.map (RelIso.toRelEmbedding φ.symm).toRelHom C

def SimpleGraph.Iso.connectedComponentEquiv {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') : G.ConnectedComponent ≃ G'.ConnectedComponent

An isomorphism of graphs induces a bijection of connected components.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_refl {V : Type u} {G : SimpleGraph V} : SimpleGraph.Iso.refl.connectedComponentEquiv = Equiv.refl G.ConnectedComponent

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_symm {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') : φ.symm.connectedComponentEquiv = φ.connectedComponentEquiv.symm

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_trans {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''} (φ : G ≃g G') (φ' : G' ≃g G'') : SimpleGraph.Iso.connectedComponentEquiv (RelIso.trans φ φ') = φ.connectedComponentEquiv.trans φ'.connectedComponentEquiv

def SimpleGraph.ConnectedComponent.supp {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) : Set V

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

Equations

• C.supp = {v : V | G.connectedComponentMk v = C}

theorem SimpleGraph.ConnectedComponent.supp_injective {V : Type u} {G : SimpleGraph V} : Function.Injective SimpleGraph.ConnectedComponent.supp

@[simp]

theorem SimpleGraph.ConnectedComponent.supp_inj {V : Type u} {G : SimpleGraph V} {C : G.ConnectedComponent} {D : G.ConnectedComponent} : C.supp = D.supp ↔ C = D

instance SimpleGraph.ConnectedComponent.instSetLike {V : Type u} {G : SimpleGraph V} : SetLike G.ConnectedComponent V

Equations

• SimpleGraph.ConnectedComponent.instSetLike = { coe := SimpleGraph.ConnectedComponent.supp, coe_injective' := ⋯ }

@[simp]

theorem SimpleGraph.ConnectedComponent.mem_supp_iff {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent) (v : V) : v ∈ C.supp ↔ G.connectedComponentMk v = C

theorem SimpleGraph.ConnectedComponent.connectedComponentMk_mem {V : Type u} {G : SimpleGraph V} {v : V} : v ∈ G.connectedComponentMk v

def SimpleGraph.ConnectedComponent.isoEquivSupp {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') (C : G.ConnectedComponent) : ↑C.supp ≃ ↑(φ.connectedComponentEquiv C).supp

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

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.ConnectedComponent.mem_coe_supp_of_adj {V : Type u} {G : SimpleGraph V} {v : V} {w : V} {H : G.Subgraph} {c : H.coe.ConnectedComponent} (hv : v ∈ Subtype.val '' ↑c) (hw : w ∈ H.verts) (hadj : H.Adj v w) : w ∈ Subtype.val '' ↑c

theorem SimpleGraph.pairwise_disjoint_supp_connectedComponent {V : Type u} (G : SimpleGraph V) : Pairwise fun (c c' : G.ConnectedComponent) => Disjoint c.supp c'.supp

theorem SimpleGraph.iUnion_connectedComponentSupp {V : Type u} (G : SimpleGraph V) : ⋃ (c : G.ConnectedComponent), c.supp = Set.univ

theorem SimpleGraph.Preconnected.set_univ_walk_nonempty {V : Type u} {G : SimpleGraph V} (hconn : G.Preconnected) (u : V) (v : V) : Set.univ.Nonempty

theorem SimpleGraph.Connected.set_univ_walk_nonempty {V : Type u} {G : SimpleGraph V} (hconn : G.Connected) (u : V) (v : V) : Set.univ.Nonempty

Bridge edges

def SimpleGraph.IsBridge {V : Type u} (G : SimpleGraph V) (e : Sym2 V) : Prop

An edge of a graph is a bridge if, after removing it, its incident vertices are no longer reachable from one another.

Equations

• G.IsBridge e = (e ∈ G.edgeSet ∧ Sym2.lift ⟨fun (v w : V) => ¬(G \ SimpleGraph.fromEdgeSet {e}).Reachable v w, ⋯⟩ e)

theorem SimpleGraph.isBridge_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : G.IsBridge s(u, v) ↔ G.Adj u v ∧ ¬(G \ SimpleGraph.fromEdgeSet {s(u, v)}).Reachable u v

theorem SimpleGraph.reachable_delete_edges_iff_exists_walk {V : Type u} {G : SimpleGraph V} {v : V} {w : V} : (G \ SimpleGraph.fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ (p : G.Walk v w), s(v, w) ∉ p.edges

theorem SimpleGraph.isBridge_iff_adj_and_forall_walk_mem_edges {V : Type u} {G : SimpleGraph V} {v : V} {w : V} : G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ (p : G.Walk v w), s(v, w) ∈ p.edges

theorem SimpleGraph.reachable_deleteEdges_iff_exists_cycle.aux {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges) (c : G.Walk u u) (hc : c.IsTrail) (he : s(v, w) ∈ c.edges) (hw : w ∈ (c.takeUntil v ⋯).support) : False

theorem SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle {V : Type u} {G : SimpleGraph V} {v : V} {w : V} : G.Adj v w ∧ (G \ SimpleGraph.fromEdgeSet {s(v, w)}).Reachable v w ↔ ∃ (u : V) (p : G.Walk u u), p.IsCycle ∧ s(v, w) ∈ p.edges

theorem SimpleGraph.isBridge_iff_adj_and_forall_cycle_not_mem {V : Type u} {G : SimpleGraph V} {v : V} {w : V} : G.IsBridge s(v, w) ↔ G.Adj v w ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → s(v, w) ∉ p.edges

theorem SimpleGraph.isBridge_iff_mem_and_forall_cycle_not_mem {V : Type u} {G : SimpleGraph V} {e : Sym2 V} : G.IsBridge e ↔ e ∈ G.edgeSet ∧ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges