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

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

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.

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

@[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 (SimpleGraph.Walk G v v)

@[match_pattern, reducible]

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

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

@[match_pattern, inline, reducible]

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

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

@[match_pattern, inline, reducible]

abbrev SimpleGraph.Walk.cons' {V : Type u} {G : SimpleGraph V} (u : V) (v : V) (w : V) (h : SimpleGraph.Adj G u v) (p : SimpleGraph.Walk G v w) : SimpleGraph.Walk G u w

Pattern to get Walk.cons with the vertices as explicit arguments.

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

@[simp]

theorem SimpleGraph.Walk.copy_rfl_rfl {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) : SimpleGraph.Walk.copy p (_ : u = u) (_ : v = v) = 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 : SimpleGraph.Walk G u v) (hu : u = u') (hv : v = v') (hu' : u' = u'') (hv' : v' = v'') : SimpleGraph.Walk.copy (SimpleGraph.Walk.copy p hu hv) hu' hv' = SimpleGraph.Walk.copy p (_ : u = u'') (_ : v = v'')

@[simp]

theorem SimpleGraph.Walk.copy_nil {V : Type u} {G : SimpleGraph V} {u : V} {u' : V} (hu : u = u') : SimpleGraph.Walk.copy SimpleGraph.Walk.nil 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 : SimpleGraph.Adj G u v) (p : SimpleGraph.Walk G v w) (hu : u = u') (hw : w = w') : SimpleGraph.Walk.copy (SimpleGraph.Walk.cons h p) hu hw = SimpleGraph.Walk.cons (_ : SimpleGraph.Adj G u' v) (SimpleGraph.Walk.copy p (_ : v = v) hw)

@[simp]

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

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

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

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

Equations

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

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

The concatenation of two compatible walks.

Equations

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

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

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

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

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

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

Equations

• SimpleGraph.Walk.reverseAux SimpleGraph.Walk.nil x = x
• SimpleGraph.Walk.reverseAux (SimpleGraph.Walk.cons h p) x = SimpleGraph.Walk.reverseAux p (SimpleGraph.Walk.cons (_ : SimpleGraph.Adj G v_3 u) x)

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

The walk in reverse.

def SimpleGraph.Walk.getVert {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : SimpleGraph.Walk G 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.getVert SimpleGraph.Walk.nil x = u
• SimpleGraph.Walk.getVert (SimpleGraph.Walk.cons h p) 0 = u
• SimpleGraph.Walk.getVert (SimpleGraph.Walk.cons h q) (Nat.succ n) = SimpleGraph.Walk.getVert q n

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem SimpleGraph.Walk.append_assoc {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} {x : V} (p : SimpleGraph.Walk G u v) (q : SimpleGraph.Walk G v w) (r : SimpleGraph.Walk G w x) : SimpleGraph.Walk.append p (SimpleGraph.Walk.append q r) = SimpleGraph.Walk.append (SimpleGraph.Walk.append p q) 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 : SimpleGraph.Walk G u v) (q : SimpleGraph.Walk G v w) (hu : u = u') (hv : v = v') (hw : w = w') : SimpleGraph.Walk.append (SimpleGraph.Walk.copy p hu hv) (SimpleGraph.Walk.copy q hv hw) = SimpleGraph.Walk.copy (SimpleGraph.Walk.append p q) hu hw

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

def SimpleGraph.Walk.concatRecAux {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → SimpleGraph.Walk G u v → Sort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : SimpleGraph.Walk G u v) → (h : SimpleGraph.Adj G v w) → motive u v p → motive u w (SimpleGraph.Walk.concat p h)) {u : V} {v : V} (p : SimpleGraph.Walk G u v) : motive v u (SimpleGraph.Walk.reverse p)

Auxiliary definition for SimpleGraph.Walk.concatRec

Equations

• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.concatRecAux Hnil Hconcat SimpleGraph.Walk.nil = Hnil u

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

@[simp]

theorem SimpleGraph.Walk.concatRec_nil {V : Type u} {G : SimpleGraph V} {motive : (u v : V) → SimpleGraph.Walk G u v → Sort u_1} (Hnil : {u : V} → motive u u SimpleGraph.Walk.nil) (Hconcat : {u v w : V} → (p : SimpleGraph.Walk G u v) → (h : SimpleGraph.Adj G v w) → motive u v p → motive u w (SimpleGraph.Walk.concat p h)) (u : V) : SimpleGraph.Walk.concatRec Hnil Hconcat SimpleGraph.Walk.nil = Hnil u

@[simp]

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

theorem SimpleGraph.Walk.concat_inj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {v' : V} {w : V} {p : SimpleGraph.Walk G u v} {h : SimpleGraph.Adj G v w} {p' : SimpleGraph.Walk G u v'} {h' : SimpleGraph.Adj G v' w} (he : SimpleGraph.Walk.concat p h = SimpleGraph.Walk.concat p' h') : ∃ hv, SimpleGraph.Walk.copy p (_ : u = u) hv = p'

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

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

Equations

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

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

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

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem SimpleGraph.Walk.mem_support_nil_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : u ∈ SimpleGraph.Walk.support SimpleGraph.Walk.nil ↔ 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 : SimpleGraph.Walk G u v) (p' : SimpleGraph.Walk G v w) : t ∈ List.tail (SimpleGraph.Walk.support (SimpleGraph.Walk.append p p')) ↔ t ∈ List.tail (SimpleGraph.Walk.support p) ∨ t ∈ List.tail (SimpleGraph.Walk.support p')

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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 : SimpleGraph.Walk G u v) (h : Quotient.mk (Sym2.Rel.setoid V) (x, y) ∈ SimpleGraph.Walk.edges p) : SimpleGraph.Adj G x y

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

@[simp]

theorem SimpleGraph.Walk.edges_cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : SimpleGraph.Adj G u v) (p : SimpleGraph.Walk G v w) : SimpleGraph.Walk.edges (SimpleGraph.Walk.cons h p) = Quotient.mk (Sym2.Rel.setoid V) (u, v) :: SimpleGraph.Walk.edges p

@[simp]

theorem SimpleGraph.Walk.edges_concat {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : SimpleGraph.Walk G u v) (h : SimpleGraph.Adj G v w) : SimpleGraph.Walk.edges (SimpleGraph.Walk.concat p h) = List.concat (SimpleGraph.Walk.edges p) (Quotient.mk (Sym2.Rel.setoid V) (v, w))

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem SimpleGraph.Walk.fst_mem_support_of_mem_edges {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : SimpleGraph.Walk G v w) (he : Quotient.mk (Sym2.Rel.setoid V) (t, u) ∈ SimpleGraph.Walk.edges p) : t ∈ SimpleGraph.Walk.support p

theorem SimpleGraph.Walk.snd_mem_support_of_mem_edges {V : Type u} {G : SimpleGraph V} {t : V} {u : V} {v : V} {w : V} (p : SimpleGraph.Walk G v w) (he : Quotient.mk (Sym2.Rel.setoid V) (t, u) ∈ SimpleGraph.Walk.edges p) : u ∈ SimpleGraph.Walk.support p

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

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

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

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

Predicate for the empty walk.

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

The second vertex along a non-nil walk.

@[simp]

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

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

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

@[simp]

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

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

The first dart of a walk.

theorem SimpleGraph.Walk.edge_firstDart {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (p : SimpleGraph.Walk G v w) (hp : ¬SimpleGraph.Walk.Nil p) : SimpleGraph.Dart.edge (SimpleGraph.Walk.firstDart p hp) = Quotient.mk (Sym2.Rel.setoid V) (v, SimpleGraph.Walk.sndOfNotNil p hp)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

Trails, paths, circuits, cycles

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

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

• edges_nodup : List.Nodup (SimpleGraph.Walk.edges p)

A trail is a walk with no repeating edges.

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

• edges_nodup : List.Nodup (SimpleGraph.Walk.edges p)
• support_nodup : List.Nodup (SimpleGraph.Walk.support p)

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

theorem SimpleGraph.Walk.IsPath.isTrail : ∀ {V : Type u_1} {G : SimpleGraph V} {a a_1 : V} {p : SimpleGraph.Walk G a a_1}, SimpleGraph.Walk.IsPath p → SimpleGraph.Walk.IsTrail p

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

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

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

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

theorem SimpleGraph.Walk.IsCircuit.isTrail : ∀ {V : Type u_1} {G : SimpleGraph V} {a : V} {p : SimpleGraph.Walk G a a}, SimpleGraph.Walk.IsCircuit p → SimpleGraph.Walk.IsTrail p

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

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

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

theorem SimpleGraph.Walk.IsCycle.isCircuit : ∀ {V : Type u_1} {G : SimpleGraph V} {a : V} {p : SimpleGraph.Walk G a a}, SimpleGraph.Walk.IsCycle p → SimpleGraph.Walk.IsCircuit p

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem SimpleGraph.Walk.cons_isTrail_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (h : SimpleGraph.Adj G u v) (p : SimpleGraph.Walk G v w) : SimpleGraph.Walk.IsTrail (SimpleGraph.Walk.cons h p) ↔ SimpleGraph.Walk.IsTrail p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ SimpleGraph.Walk.edges p

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

theorem SimpleGraph.Walk.IsPath.cons {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : ∀ {a : V} {p : SimpleGraph.Walk G v a}, SimpleGraph.Walk.IsPath p → ¬u ∈ SimpleGraph.Walk.support p → ∀ {h : SimpleGraph.Adj G u v}, SimpleGraph.Walk.IsPath (SimpleGraph.Walk.cons h p)

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

theorem SimpleGraph.Walk.cons_isCycle_iff {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G v u) (h : SimpleGraph.Adj G u v) : SimpleGraph.Walk.IsCycle (SimpleGraph.Walk.cons h p) ↔ SimpleGraph.Walk.IsPath p ∧ ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ SimpleGraph.Walk.edges p

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

About paths

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

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

Walk decompositions

def SimpleGraph.Walk.takeUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : V} (p : SimpleGraph.Walk G v w) (u : V) : u ∈ SimpleGraph.Walk.support p → SimpleGraph.Walk G 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.takeUntil SimpleGraph.Walk.nil x x_1 = Eq.mpr (_ : SimpleGraph.Walk G v x = SimpleGraph.Walk G v v) SimpleGraph.Walk.nil

def SimpleGraph.Walk.dropUntil {V : Type u} {G : SimpleGraph V} [DecidableEq V] {v : V} {w : V} (p : SimpleGraph.Walk G v w) (u : V) : u ∈ SimpleGraph.Walk.support p → SimpleGraph.Walk G 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.dropUntil SimpleGraph.Walk.nil x x_1 = Eq.mpr (_ : SimpleGraph.Walk G x v = SimpleGraph.Walk G v v) SimpleGraph.Walk.nil

@[simp]

theorem SimpleGraph.Walk.take_spec {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : SimpleGraph.Walk G v w) (h : u ∈ SimpleGraph.Walk.support p) : SimpleGraph.Walk.append (SimpleGraph.Walk.takeUntil p u h) (SimpleGraph.Walk.dropUntil p 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 : SimpleGraph.Walk G u v} : w ∈ SimpleGraph.Walk.support p ↔ ∃ q r, p = SimpleGraph.Walk.append q 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 : SimpleGraph.Walk G v w) (h : u ∈ SimpleGraph.Walk.support p) : List.count u (SimpleGraph.Walk.support (SimpleGraph.Walk.takeUntil p u h)) = 1

theorem SimpleGraph.Walk.count_edges_takeUntil_le_one {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u : V} {v : V} {w : V} (p : SimpleGraph.Walk G v w) (h : u ∈ SimpleGraph.Walk.support p) (x : V) : List.count (Quotient.mk (Sym2.Rel.setoid V) (u, x)) (SimpleGraph.Walk.edges (SimpleGraph.Walk.takeUntil p u h)) ≤ 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 : SimpleGraph.Walk G v w) (hv : v = v') (hw : w = w') (h : u ∈ SimpleGraph.Walk.support (SimpleGraph.Walk.copy p hv hw)) : SimpleGraph.Walk.takeUntil (SimpleGraph.Walk.copy p hv hw) u h = SimpleGraph.Walk.copy (SimpleGraph.Walk.takeUntil p u (_ : u ∈ SimpleGraph.Walk.support p)) hv (_ : u = u)

@[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 : SimpleGraph.Walk G v w) (hv : v = v') (hw : w = w') (h : u ∈ SimpleGraph.Walk.support (SimpleGraph.Walk.copy p hv hw)) : SimpleGraph.Walk.dropUntil (SimpleGraph.Walk.copy p hv hw) u h = SimpleGraph.Walk.copy (SimpleGraph.Walk.dropUntil p u (_ : u ∈ SimpleGraph.Walk.support p)) (_ : u = u) hw

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

theorem SimpleGraph.Walk.exists_boundary_dart {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) (S : Set V) (uS : u ∈ S) (vS : ¬v ∈ S) : ∃ d, d ∈ SimpleGraph.Walk.darts p ∧ d.fst ∈ S ∧ ¬d.snd ∈ 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

@[inline, reducible]

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

The type for paths between two vertices.

@[simp]

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

@[simp]

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

@[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} : SimpleGraph.Path G u u

The length-0 path at a vertex.

@[simp]

theorem SimpleGraph.Path.singleton_coe {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : SimpleGraph.Adj G 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 : SimpleGraph.Adj G u v) : SimpleGraph.Path G u v

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

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

@[simp]

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

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

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

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

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

@[simp]

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

theorem SimpleGraph.Path.loop_eq {V : Type u} {G : SimpleGraph V} {v : V} (p : SimpleGraph.Path G 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 : SimpleGraph.Path G v v} : ¬e ∈ SimpleGraph.Walk.edges ↑p

theorem SimpleGraph.Path.cons_isCycle {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Path G v u) (h : SimpleGraph.Adj G u v) (he : ¬Quotient.mk (Sym2.Rel.setoid V) (u, v) ∈ SimpleGraph.Walk.edges ↑p) : SimpleGraph.Walk.IsCycle (SimpleGraph.Walk.cons h ↑p)

Walks to paths

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

• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.bypass SimpleGraph.Walk.nil = SimpleGraph.Walk.nil

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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} : SimpleGraph.Walk G u v → SimpleGraph.Walk G' (↑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.Adj G' (↑f u) (↑f v_3)) (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 : SimpleGraph.Walk G u v) {w : V} (h : SimpleGraph.Adj G w u) : SimpleGraph.Walk.map f (SimpleGraph.Walk.cons h p) = SimpleGraph.Walk.cons (_ : SimpleGraph.Adj G' (↑f w) (↑f u)) (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 : SimpleGraph.Walk G u v) (hu : u = u') (hv : v = v') : SimpleGraph.Walk.map f (SimpleGraph.Walk.copy p hu hv) = SimpleGraph.Walk.copy (SimpleGraph.Walk.map f p) (_ : ↑f u = ↑f u') (_ : ↑f v = ↑f v')

@[simp]

theorem SimpleGraph.Walk.map_id {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) (p : SimpleGraph.Walk G 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 : SimpleGraph.Walk G u v) : SimpleGraph.Walk.map f' (SimpleGraph.Walk.map f p) = SimpleGraph.Walk.map (SimpleGraph.Hom.comp f' 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 : SimpleGraph.Walk G u v) {f : G →g G'} (f' : G →g G') (h : f = f') : SimpleGraph.Walk.map f p = SimpleGraph.Walk.copy (SimpleGraph.Walk.map f' p) (_ : ↑f' u = ↑f u) (_ : ↑f' v = ↑f v)

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 : SimpleGraph.Walk G 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 : SimpleGraph.Walk G u v) : SimpleGraph.Walk.length (SimpleGraph.Walk.map f p) = SimpleGraph.Walk.length p

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 : SimpleGraph.Walk G u v) (q : SimpleGraph.Walk G v w) : SimpleGraph.Walk.map f (SimpleGraph.Walk.append p q) = SimpleGraph.Walk.append (SimpleGraph.Walk.map f p) (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 : SimpleGraph.Walk G u v) : SimpleGraph.Walk.reverse (SimpleGraph.Walk.map f p) = SimpleGraph.Walk.map f (SimpleGraph.Walk.reverse p)

@[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 : SimpleGraph.Walk G u v) : SimpleGraph.Walk.support (SimpleGraph.Walk.map f p) = List.map (↑f) (SimpleGraph.Walk.support p)

@[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 : SimpleGraph.Walk G u v) : SimpleGraph.Walk.darts (SimpleGraph.Walk.map f p) = List.map (SimpleGraph.Hom.mapDart f) (SimpleGraph.Walk.darts p)

@[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 : SimpleGraph.Walk G u v) : SimpleGraph.Walk.edges (SimpleGraph.Walk.map f p) = List.map (Sym2.map ↑f) (SimpleGraph.Walk.edges p)

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 : SimpleGraph.Walk G u v} (hinj : Function.Injective ↑f) (hp : SimpleGraph.Walk.IsPath p) : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.map f p)

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

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 : SimpleGraph.Walk G u v} (hinj : Function.Injective ↑f) : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.map f p) ↔ SimpleGraph.Walk.IsPath p

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 : SimpleGraph.Walk G u v} (hinj : Function.Injective ↑f) : SimpleGraph.Walk.IsTrail (SimpleGraph.Walk.map f p) ↔ SimpleGraph.Walk.IsTrail p

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 : SimpleGraph.Walk G u v} (hinj : Function.Injective ↑f) : SimpleGraph.Walk.IsTrail p → SimpleGraph.Walk.IsTrail (SimpleGraph.Walk.map f p)

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 : SimpleGraph.Walk G u u} (hinj : Function.Injective ↑f) : SimpleGraph.Walk.IsCycle (SimpleGraph.Walk.map f p) ↔ SimpleGraph.Walk.IsCycle p

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

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]

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

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

@[simp]

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

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

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 : SimpleGraph.Walk G u v} : SimpleGraph.Walk.IsTrail (SimpleGraph.Walk.mapLe h p) → SimpleGraph.Walk.IsTrail p

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 : SimpleGraph.Walk G u v} : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.mapLe h p) ↔ SimpleGraph.Walk.IsPath p

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

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 : SimpleGraph.Walk G u v} : SimpleGraph.Walk.IsPath p → SimpleGraph.Walk.IsPath (SimpleGraph.Walk.mapLe h p)

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 : SimpleGraph.Walk G u u} : SimpleGraph.Walk.IsCycle (SimpleGraph.Walk.mapLe h p) ↔ SimpleGraph.Walk.IsCycle p

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

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 : SimpleGraph.Walk G u u} : SimpleGraph.Walk.IsCycle p → SimpleGraph.Walk.IsCycle (SimpleGraph.Walk.mapLe h p)

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 : SimpleGraph.Path G 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 : SimpleGraph.Path G u v) : SimpleGraph.Path G' (↑f u) (↑f v)

Given an injective graph homomorphism, map paths to paths.

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 : SimpleGraph.Path G u v) : ↑(SimpleGraph.Path.mapEmbedding f p) = SimpleGraph.Walk.map (SimpleGraph.Embedding.toHom f) ↑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 : SimpleGraph.Path G u v) : SimpleGraph.Path G' (↑f u) (↑f v)

Given a graph embedding, map paths to paths.

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 : SimpleGraph.Walk G u v) (H : SimpleGraph V) (h : ∀ (e : Sym2 V), e ∈ SimpleGraph.Walk.edges p → e ∈ SimpleGraph.edgeSet H) : SimpleGraph.Walk H u v

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

Equations

• One or more equations did not get rendered due to their size.
• SimpleGraph.Walk.transfer SimpleGraph.Walk.nil H h_2 = SimpleGraph.Walk.nil

theorem SimpleGraph.Walk.transfer_self {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) : SimpleGraph.Walk.transfer p G (_ : ∀ ⦃e : Sym2 V⦄, e ∈ SimpleGraph.Walk.edges p → e ∈ SimpleGraph.edgeSet G) = p

theorem SimpleGraph.Walk.transfer_eq_map_of_le {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) {H : SimpleGraph V} (hp : ∀ (e : Sym2 V), e ∈ SimpleGraph.Walk.edges p → e ∈ SimpleGraph.edgeSet H) (GH : G ≤ H) : SimpleGraph.Walk.transfer p 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 : SimpleGraph.Walk G u v) {H : SimpleGraph V} (hp : ∀ (e : Sym2 V), e ∈ SimpleGraph.Walk.edges p → e ∈ SimpleGraph.edgeSet H) : SimpleGraph.Walk.edges (SimpleGraph.Walk.transfer p H hp) = SimpleGraph.Walk.edges p

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

Deleting edges

@[reducible]

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

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

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_nil {V : Type u} {G : SimpleGraph V} (s : Set (Sym2 V)) {v : V} (hp : ∀ (e : Sym2 V), e ∈ SimpleGraph.Walk.edges SimpleGraph.Walk.nil → ¬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 : SimpleGraph.Adj G u v) (p : SimpleGraph.Walk G v w) (hp : ∀ (e : Sym2 V), e ∈ SimpleGraph.Walk.edges (SimpleGraph.Walk.cons h p) → ¬e ∈ s) : SimpleGraph.Walk.toDeleteEdges s (SimpleGraph.Walk.cons h p) hp = SimpleGraph.Walk.cons (_ : SimpleGraph.Adj (SimpleGraph.deleteEdges G s) u v) (SimpleGraph.Walk.toDeleteEdges s p fun x he => hp x (_ : List.Mem x (SimpleGraph.Dart.edge { toProd := (u, v), is_adj := h } :: List.map SimpleGraph.Dart.edge (SimpleGraph.Walk.darts p))))

@[inline, reducible]

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

@[simp]

theorem SimpleGraph.Walk.map_toDeleteEdges_eq {V : Type u} {G : SimpleGraph V} {v : V} {w : V} (s : Set (Sym2 V)) {p : SimpleGraph.Walk G v w} (hp : ∀ (e : Sym2 V), e ∈ SimpleGraph.Walk.edges p → ¬e ∈ s) : SimpleGraph.Walk.map (SimpleGraph.Hom.mapSpanningSubgraphs (_ : SimpleGraph.deleteEdges G s ≤ G)) (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 : SimpleGraph.Walk G v w} (h : SimpleGraph.Walk.IsPath p) (hp : ∀ (e : Sym2 V), e ∈ SimpleGraph.Walk.edges p → ¬e ∈ s) : SimpleGraph.Walk.IsPath (SimpleGraph.Walk.toDeleteEdges s p hp)

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

@[simp]

theorem SimpleGraph.Walk.toDeleteEdges_copy {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {u' : V} {v' : V} (s : Set (Sym2 V)) (p : SimpleGraph.Walk G u v) (hu : u = u') (hv : v = v') (h : ∀ (e : Sym2 V), e ∈ SimpleGraph.Walk.edges (SimpleGraph.Walk.copy p hu hv) → ¬e ∈ s) : SimpleGraph.Walk.toDeleteEdges s (SimpleGraph.Walk.copy p hu hv) h = SimpleGraph.Walk.copy (SimpleGraph.Walk.toDeleteEdges s p (_ : ∀ (e : Sym2 V), e ∈ SimpleGraph.Walk.edges p → ¬e ∈ s)) 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.

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

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

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

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

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

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

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

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

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

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

theorem SimpleGraph.reachable_iff_reflTransGen {V : Type u} {G : SimpleGraph V} (u : V) (v : V) : SimpleGraph.Reachable G 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 : SimpleGraph.Reachable G u v) : SimpleGraph.Reachable G' (↑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 : SimpleGraph.Reachable G u v) : SimpleGraph.Reachable G' 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} : SimpleGraph.Reachable G' (↑φ u) (↑φ v) ↔ SimpleGraph.Reachable G 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'} : SimpleGraph.Reachable G (↑(SimpleGraph.Iso.symm φ) v) u ↔ SimpleGraph.Reachable G' v (↑φ u)

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

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

The equivalence relation on vertices given by SimpleGraph.Reachable.

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

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

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 : SimpleGraph.Preconnected G) : SimpleGraph.Preconnected H

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

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

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

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

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

• preconnected : SimpleGraph.Preconnected G
• nonempty : Nonempty V

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.

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

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

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 : SimpleGraph.Connected G) : SimpleGraph.Connected H

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

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

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

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.

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

Gives the connected component containing a particular vertex.

@[simp]

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

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

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

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

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

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

@[simp]

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

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

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

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

@[simp]

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

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

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

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

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

The map on connected components induced by a graph homomorphism.

@[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 φ (SimpleGraph.connectedComponentMk G v) = SimpleGraph.connectedComponentMk G' (↑φ v)

@[simp]

theorem SimpleGraph.ConnectedComponent.map_id {V : Type u} {G : SimpleGraph V} (C : SimpleGraph.ConnectedComponent G) : 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 : SimpleGraph.ConnectedComponent G) (φ : G →g G') (ψ : G' →g G'') : SimpleGraph.ConnectedComponent.map ψ (SimpleGraph.ConnectedComponent.map φ C) = SimpleGraph.ConnectedComponent.map (SimpleGraph.Hom.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 : SimpleGraph.ConnectedComponent G} : SimpleGraph.connectedComponentMk G' (↑φ v) = SimpleGraph.ConnectedComponent.map (RelEmbedding.toRelHom (RelIso.toRelEmbedding φ)) C ↔ SimpleGraph.connectedComponentMk G 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 : SimpleGraph.ConnectedComponent G} : SimpleGraph.connectedComponentMk G (↑(SimpleGraph.Iso.symm φ) v') = C ↔ SimpleGraph.connectedComponentMk G' v' = SimpleGraph.ConnectedComponent.map (RelEmbedding.toRelHom (RelIso.toRelEmbedding φ)) C

@[simp]

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

@[simp]

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

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

An isomorphism of graphs induces a bijection of connected components.

@[simp]

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

@[simp]

theorem SimpleGraph.Iso.connectedComponentEquiv_symm {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G ≃g G') : SimpleGraph.Iso.connectedComponentEquiv (SimpleGraph.Iso.symm φ) = (SimpleGraph.Iso.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 φ φ') = (SimpleGraph.Iso.connectedComponentEquiv φ).trans (SimpleGraph.Iso.connectedComponentEquiv φ')

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

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

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 : SimpleGraph.ConnectedComponent G} {D : SimpleGraph.ConnectedComponent G} : SimpleGraph.ConnectedComponent.supp C = SimpleGraph.ConnectedComponent.supp D ↔ C = D

instance SimpleGraph.ConnectedComponent.instSetLikeConnectedComponent {V : Type u} {G : SimpleGraph V} : SetLike (SimpleGraph.ConnectedComponent G) V

@[simp]

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

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

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

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

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

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

Walks as subgraphs

def SimpleGraph.Walk.toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} : SimpleGraph.Walk G u v → SimpleGraph.Subgraph G

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

Equations

• SimpleGraph.Walk.toSubgraph SimpleGraph.Walk.nil = SimpleGraph.singletonSubgraph G u
• SimpleGraph.Walk.toSubgraph (SimpleGraph.Walk.cons h q) = SimpleGraph.subgraphOfAdj G h ⊔ SimpleGraph.Walk.toSubgraph q

theorem SimpleGraph.Walk.toSubgraph_cons_nil_eq_subgraphOfAdj {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (h : SimpleGraph.Adj G u v) : SimpleGraph.Walk.toSubgraph (SimpleGraph.Walk.cons h SimpleGraph.Walk.nil) = SimpleGraph.subgraphOfAdj G h

theorem SimpleGraph.Walk.mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} {w : V} (p : SimpleGraph.Walk G u v) : w ∈ (SimpleGraph.Walk.toSubgraph p).verts ↔ w ∈ SimpleGraph.Walk.support p

theorem SimpleGraph.Walk.start_mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) : u ∈ (SimpleGraph.Walk.toSubgraph p).verts

theorem SimpleGraph.Walk.end_mem_verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) : v ∈ (SimpleGraph.Walk.toSubgraph p).verts

@[simp]

theorem SimpleGraph.Walk.verts_toSubgraph {V : Type u} {G : SimpleGraph V} {u : V} {v : V} (p : SimpleGraph.Walk G u v) : (SimpleGraph.Walk.toSubgraph p).verts = {w | w ∈ SimpleGraph.Walk.support p}

theorem SimpleGraph.Walk.mem_edges_toSubgraph {V : Type u} {G : SimpleGraph V} {u :