mathlib3 documentation

combinatorics.simple_graph.connectivity

Graph connectivity #

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

In a simple graph,

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

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

Main definitions #

Main statements #

Tags #

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

source
inductive simple_graph.walk {V : Type u} (G : simple_graph V) :
V → V → Type u

A walk is a sequence of adjacent vertices. For vertices u v : V, the type walk u v consists of all walks starting at u and ending at v.

We say that a walk visits the vertices it contains. The set of vertices a walk visits is simple_graph.walk.support.

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

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

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

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

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

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

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

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

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

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

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

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

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

The concatenation of two compatible walks.

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

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

Equations
source
theorem simple_graph.walk.concat_eq_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
p.concat h = p.append (simple_graph.walk.cons h simple_graph.walk.nil)
source
@[protected]
def simple_graph.walk.reverse_aux {V : Type u} {G : simple_graph V} {u v w : V} :
G.walk u v → G.walk u w → G.walk v w

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

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

The walk in reverse.

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

Get the 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
source
@[simp]
theorem simple_graph.walk.get_vert_zero {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) :
w.get_vert 0 = u
source
theorem simple_graph.walk.get_vert_of_length_le {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) {i : ℕ} (hi : w.length ≤ i) :
w.get_vert i = v
source
@[simp]
theorem simple_graph.walk.get_vert_length {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) :
w.get_vert w.length = v
source
theorem simple_graph.walk.adj_get_vert_succ {V : Type u} {G : simple_graph V} {u v : V} (w : G.walk u v) {i : ℕ} (hi : i < w.length) :
G.adj (w.get_vert i) (w.get_vert (i + 1))
source
@[simp]
theorem simple_graph.walk.cons_append {V : Type u} {G : simple_graph V} {u v w x : V} (h : G.adj u v) (p : G.walk v w) (q : G.walk w x) :
(simple_graph.walk.cons h p).append q = simple_graph.walk.cons h (p.append q)
source
@[simp]
theorem simple_graph.walk.cons_nil_append {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
(simple_graph.walk.cons h simple_graph.walk.nil).append p = simple_graph.walk.cons h p
source
@[simp]
theorem simple_graph.walk.append_nil {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.append simple_graph.walk.nil = p
source
@[simp]
theorem simple_graph.walk.nil_append {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
simple_graph.walk.nil.append p = p
source
theorem simple_graph.walk.append_assoc {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk v w) (r : G.walk w x) :
p.append (q.append r) = (p.append q).append r
source
@[simp]
theorem simple_graph.walk.append_copy_copy {V : Type u} {G : simple_graph V} {u v w u' v' w' : V} (p : G.walk u v) (q : G.walk v w) (hu : u = u') (hv : v = v') (hw : w = w') :
(p.copy hu hv).append (q.copy hv hw) = (p.append q).copy hu hw
source
theorem simple_graph.walk.concat_nil {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
simple_graph.walk.nil.concat h = simple_graph.walk.cons h simple_graph.walk.nil
source
@[simp]
theorem simple_graph.walk.concat_cons {V : Type u} {G : simple_graph V} {u v w x : V} (h : G.adj u v) (p : G.walk v w) (h' : G.adj w x) :
(simple_graph.walk.cons h p).concat h' = simple_graph.walk.cons h (p.concat h')
source
theorem simple_graph.walk.append_concat {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (q : G.walk v w) (h : G.adj w x) :
p.append (q.concat h) = (p.append q).concat h
source
theorem simple_graph.walk.concat_append {V : Type u} {G : simple_graph V} {u v w x : V} (p : G.walk u v) (h : G.adj v w) (q : G.walk w x) :
(p.concat h).append q = p.append (simple_graph.walk.cons h q)
source
theorem simple_graph.walk.exists_cons_eq_concat {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
∃ (x : V) (q : G.walk u x) (h' : G.adj x w), simple_graph.walk.cons h p = q.concat h'

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

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

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

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

Auxiliary definition for simple_graph.walk.concat_rec

Equations
source
def simple_graph.walk.concat_rec {V : Type u} {G : simple_graph V} {motive : Π (u v : V), G.walk u v → Sort u_1} (Hnil : Π {u : V}, motive u u simple_graph.walk.nil) (Hconcat : Π {u v w : V} (p : G.walk u v) (h : G.adj v w), motive u v p → motive u w (p.concat h)) {u v : V} (p : G.walk u v) :
motive u v p

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

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

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

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

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

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

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

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

Equations
source
@[simp]
theorem simple_graph.walk.support_nil {V : Type u} {G : simple_graph V} {u : V} :
simple_graph.walk.nil.support = [u]
source
@[simp]
theorem simple_graph.walk.support_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
(simple_graph.walk.cons h p).support = u :: p.support
source
@[simp]
theorem simple_graph.walk.support_concat {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
(p.concat h).support = p.support.concat w
source
@[simp]
theorem simple_graph.walk.support_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).support = p.support
source
theorem simple_graph.walk.support_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
(p.append p').support = p.support ++ p'.support.tail
source
@[simp]
theorem simple_graph.walk.support_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.reverse.support = p.support.reverse
source
theorem simple_graph.walk.support_ne_nil {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.support ≠ list.nil
source
theorem simple_graph.walk.tail_support_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
(p.append p').support.tail = p.support.tail ++ p'.support.tail
source
theorem simple_graph.walk.support_eq_cons {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.support = u :: p.support.tail
source
@[simp]
theorem simple_graph.walk.start_mem_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
u ∈ p.support
source
@[simp]
theorem simple_graph.walk.end_mem_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
v ∈ p.support
source
@[simp]
theorem simple_graph.walk.support_nonempty {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
{w : V | w ∈ p.support}.nonempty
source
theorem simple_graph.walk.mem_support_iff {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) :
w ∈ p.support ↔ w = u ∨ w ∈ p.support.tail
source
theorem simple_graph.walk.mem_support_nil_iff {V : Type u} {G : simple_graph V} {u v : V} :
u ∈ simple_graph.walk.nil.support ↔ u = v
source
@[simp]
theorem simple_graph.walk.mem_tail_support_append_iff {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk u v) (p' : G.walk v w) :
t ∈ (p.append p').support.tail ↔ t ∈ p.support.tail ∨ t ∈ p'.support.tail
source
@[simp]
theorem simple_graph.walk.end_mem_tail_support_of_ne {V : Type u} {G : simple_graph V} {u v : V} (h : u ≠ v) (p : G.walk u v) :
v ∈ p.support.tail
source
@[simp]
theorem simple_graph.walk.mem_support_append_iff {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk u v) (p' : G.walk v w) :
t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support
source
@[simp]
theorem simple_graph.walk.subset_support_append_left {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
p.support ⊆ (p.append q).support
source
@[simp]
theorem simple_graph.walk.subset_support_append_right {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
q.support ⊆ (p.append q).support
source
theorem simple_graph.walk.coe_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
↑(p.support) = {u} + ↑(p.support.tail)
source
theorem simple_graph.walk.coe_support_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
↑((p.append p').support) = {u} + ↑(p.support.tail) + ↑(p'.support.tail)
source
theorem simple_graph.walk.coe_support_append' {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
↑((p.append p').support) = ↑(p.support) + ↑(p'.support) - {v}
source
theorem simple_graph.walk.chain_adj_support {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
list.chain G.adj u p.support
source
theorem simple_graph.walk.chain'_adj_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
list.chain' G.adj p.support
source
theorem simple_graph.walk.chain_dart_adj_darts {V : Type u} {G : simple_graph V} {d : G.dart} {v w : V} (h : d.to_prod.snd = v) (p : G.walk v w) :
list.chain G.dart_adj d p.darts
source
theorem simple_graph.walk.chain'_dart_adj_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
list.chain' G.dart_adj p.darts
source
theorem simple_graph.walk.edges_subset_edge_set {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) ⦃e : sym2 V⦄ (h : e ∈ p.edges) :
e ∈ ⇑simple_graph.edge_set 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.

source
theorem simple_graph.walk.adj_of_mem_edges {V : Type u} {G : simple_graph V} {u v x y : V} (p : G.walk u v) (h : ⟦(x, y)⟧ ∈ p.edges) :
G.adj x y
source
@[simp]
theorem simple_graph.walk.darts_nil {V : Type u} {G : simple_graph V} {u : V} :
simple_graph.walk.nil.darts = list.nil
source
@[simp]
theorem simple_graph.walk.darts_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
(simple_graph.walk.cons h p).darts = {to_prod := (u, v), is_adj := h} :: p.darts
source
@[simp]
theorem simple_graph.walk.darts_concat {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
(p.concat h).darts = p.darts.concat {to_prod := (v, w), is_adj := h}
source
@[simp]
theorem simple_graph.walk.darts_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).darts = p.darts
source
@[simp]
theorem simple_graph.walk.darts_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
(p.append p').darts = p.darts ++ p'.darts
source
@[simp]
theorem simple_graph.walk.darts_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.reverse.darts = (list.map simple_graph.dart.symm p.darts).reverse
source
theorem simple_graph.walk.mem_darts_reverse {V : Type u} {G : simple_graph V} {u v : V} {d : G.dart} {p : G.walk u v} :
d ∈ p.reverse.darts ↔ d.symm ∈ p.darts
source
theorem simple_graph.walk.cons_map_snd_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
u :: list.map simple_graph.dart.snd p.darts = p.support
source
theorem simple_graph.walk.map_snd_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
list.map simple_graph.dart.snd p.darts = p.support.tail
source
theorem simple_graph.walk.map_fst_darts_append {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
list.map simple_graph.dart.fst p.darts ++ [v] = p.support
source
theorem simple_graph.walk.map_fst_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
list.map simple_graph.dart.fst p.darts = p.support.init
source
@[simp]
theorem simple_graph.walk.edges_nil {V : Type u} {G : simple_graph V} {u : V} :
simple_graph.walk.nil.edges = list.nil
source
@[simp]
theorem simple_graph.walk.edges_cons {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
(simple_graph.walk.cons h p).edges = ⟦(u, v)⟧ :: p.edges
source
@[simp]
theorem simple_graph.walk.edges_concat {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (h : G.adj v w) :
(p.concat h).edges = p.edges.concat ⟦(v, w)⟧
source
@[simp]
theorem simple_graph.walk.edges_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).edges = p.edges
source
@[simp]
theorem simple_graph.walk.edges_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (p' : G.walk v w) :
(p.append p').edges = p.edges ++ p'.edges
source
@[simp]
theorem simple_graph.walk.edges_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.reverse.edges = p.edges.reverse
source
@[simp]
theorem simple_graph.walk.length_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.support.length = p.length + 1
source
@[simp]
theorem simple_graph.walk.length_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.darts.length = p.length
source
@[simp]
theorem simple_graph.walk.length_edges {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.edges.length = p.length
source
theorem simple_graph.walk.dart_fst_mem_support_of_mem_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {d : G.dart} :
d ∈ p.darts → d.to_prod.fst ∈ p.support
source
theorem simple_graph.walk.dart_snd_mem_support_of_mem_darts {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {d : G.dart} (h : d ∈ p.darts) :
d.to_prod.snd ∈ p.support
source
theorem simple_graph.walk.fst_mem_support_of_mem_edges {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk v w) (he : ⟦(t, u)⟧ ∈ p.edges) :
t ∈ p.support
source
theorem simple_graph.walk.snd_mem_support_of_mem_edges {V : Type u} {G : simple_graph V} {t u v w : V} (p : G.walk v w) (he : ⟦(t, u)⟧ ∈ p.edges) :
u ∈ p.support
source
theorem simple_graph.walk.darts_nodup_of_support_nodup {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.support.nodup) :
p.darts.nodup
source
theorem simple_graph.walk.edges_nodup_of_support_nodup {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.support.nodup) :
p.edges.nodup

Trails, paths, circuits, cycles #

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

A trail is a walk with no repeating edges.

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

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

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

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

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

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

source
theorem simple_graph.walk.is_trail_def {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.is_trail ↔ p.edges.nodup
source
@[simp]
theorem simple_graph.walk.is_trail_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).is_trail ↔ p.is_trail
source
theorem simple_graph.walk.is_path.mk' {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.support.nodup) :
p.is_path
source
theorem simple_graph.walk.is_path_def {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.is_path ↔ p.support.nodup
source
@[simp]
theorem simple_graph.walk.is_path_copy {V : Type u} {G : simple_graph V} {u v u' v' : V} (p : G.walk u v) (hu : u = u') (hv : v = v') :
(p.copy hu hv).is_path ↔ p.is_path
source
theorem simple_graph.walk.is_circuit_def {V : Type u} {G : simple_graph V} {u : V} (p : G.walk u u) :
p.is_circuit ↔ p.is_trail ∧ p ≠ simple_graph.walk.nil
source
@[simp]
theorem simple_graph.walk.is_circuit_copy {V : Type u} {G : simple_graph V} {u u' : V} (p : G.walk u u) (hu : u = u') :
(p.copy hu hu).is_circuit ↔ p.is_circuit
source
theorem simple_graph.walk.is_cycle_def {V : Type u} {G : simple_graph V} {u : V} (p : G.walk u u) :
p.is_cycle ↔ p.is_trail ∧ p ≠ simple_graph.walk.nil ∧ p.support.tail.nodup
source
@[simp]
theorem simple_graph.walk.is_cycle_copy {V : Type u} {G : simple_graph V} {u u' : V} (p : G.walk u u) (hu : u = u') :
(p.copy hu hu).is_cycle ↔ p.is_cycle
source
@[simp]
theorem simple_graph.walk.is_trail.nil {V : Type u} {G : simple_graph V} {u : V} :
simple_graph.walk.nil.is_trail
source
theorem simple_graph.walk.is_trail.of_cons {V : Type u} {G : simple_graph V} {u v w : V} {h : G.adj u v} {p : G.walk v w} :
(simple_graph.walk.cons h p).is_trail → p.is_trail
source
@[simp]
theorem simple_graph.walk.cons_is_trail_iff {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
(simple_graph.walk.cons h p).is_trail ↔ p.is_trail ∧ ⟦(u, v)⟧ ∉ p.edges
source
theorem simple_graph.walk.is_trail.reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) (h : p.is_trail) :
p.reverse.is_trail
source
@[simp]
theorem simple_graph.walk.reverse_is_trail_iff {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.reverse.is_trail ↔ p.is_trail
source
theorem simple_graph.walk.is_trail.of_append_left {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} (h : (p.append q).is_trail) :
p.is_trail
source
theorem simple_graph.walk.is_trail.of_append_right {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} (h : (p.append q).is_trail) :
q.is_trail
source
theorem simple_graph.walk.is_trail.count_edges_le_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_trail) (e : sym2 V) :
list.count e p.edges ≤ 1
source
theorem simple_graph.walk.is_trail.count_edges_eq_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.walk u v} (h : p.is_trail) {e : sym2 V} (he : e ∈ p.edges) :
list.count e p.edges = 1
source
theorem simple_graph.walk.is_path.nil {V : Type u} {G : simple_graph V} {u : V} :
simple_graph.walk.nil.is_path
source
theorem simple_graph.walk.is_path.of_cons {V : Type u} {G : simple_graph V} {u v w : V} {h : G.adj u v} {p : G.walk v w} :
(simple_graph.walk.cons h p).is_path → p.is_path
source
@[simp]
theorem simple_graph.walk.cons_is_path_iff {V : Type u} {G : simple_graph V} {u v w : V} (h : G.adj u v) (p : G.walk v w) :
(simple_graph.walk.cons h p).is_path ↔ p.is_path ∧ u ∉ p.support
source
@[simp]
theorem simple_graph.walk.is_path_iff_eq_nil {V : Type u} {G : simple_graph V} {u : V} (p : G.walk u u) :
p.is_path ↔ p = simple_graph.walk.nil
source
theorem simple_graph.walk.is_path.reverse {V : Type u} {G : simple_graph V} {u v : V} {p : G.walk u v} (h : p.is_path) :
p.reverse.is_path
source
@[simp]
theorem simple_graph.walk.is_path_reverse_iff {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.reverse.is_path ↔ p.is_path
source
theorem simple_graph.walk.is_path.of_append_left {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} :
(p.append q).is_path → p.is_path
source
theorem simple_graph.walk.is_path.of_append_right {V : Type u} {G : simple_graph V} {u v w : V} {p : G.walk u v} {q : G.walk v w} (h : (p.append q).is_path) :
q.is_path
source
@[simp]
theorem simple_graph.walk.is_cycle.not_of_nil {V : Type u} {G : simple_graph V} {u : V} :
¬simple_graph.walk.nil.is_cycle
source
theorem simple_graph.walk.cons_is_cycle_iff {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk v u) (h : G.adj u v) :
(simple_graph.walk.cons h p).is_cycle ↔ p.is_path ∧ ⟦(u, v)⟧ ∉ p.edges

About paths #

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

Walk decompositions #

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

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

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

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

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

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

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

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

Equations
source
@[simp]
theorem simple_graph.walk.support_rotate {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (c : G.walk v v) (h : u ∈ c.support) :
(c.rotate h).support.tail ~r c.support.tail
source
theorem simple_graph.walk.rotate_darts {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (c : G.walk v v) (h : u ∈ c.support) :
(c.rotate h).darts ~r c.darts
source
theorem simple_graph.walk.rotate_edges {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (c : G.walk v v) (h : u ∈ c.support) :
(c.rotate h).edges ~r c.edges
source
@[protected]
theorem simple_graph.walk.is_trail.rotate {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {c : G.walk v v} (hc : c.is_trail) (h : u ∈ c.support) :
(c.rotate h).is_trail
source
@[protected]
theorem simple_graph.walk.is_circuit.rotate {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {c : G.walk v v} (hc : c.is_circuit) (h : u ∈ c.support) :
(c.rotate h).is_circuit
source
@[protected]
theorem simple_graph.walk.is_cycle.rotate {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {c : G.walk v v} (hc : c.is_cycle) (h : u ∈ c.support) :
(c.rotate h).is_cycle
source
theorem simple_graph.walk.exists_boundary_dart {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) (S : set V) (uS : u ∈ S) (vS : v ∉ S) :
∃ (d : G.dart), d ∈ p.darts ∧ d.to_prod.fst ∈ S ∧ d.to_prod.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 #

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

The type for paths between two vertices.

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

The length-0 path at a vertex.

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

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

Equations
source
@[simp]
theorem simple_graph.path.singleton_coe {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
↑(simple_graph.path.singleton h) = simple_graph.walk.cons h simple_graph.walk.nil
source
theorem simple_graph.path.mk_mem_edges_singleton {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
⟦(u, v)⟧ ∈ ↑(simple_graph.path.singleton h).edges
source
@[simp]
theorem simple_graph.path.reverse_coe {V : Type u} {G : simple_graph V} {u v : V} (p : G.path u v) :
↑(p.reverse) = ↑p.reverse
source
@[symm]
def simple_graph.path.reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.path u v) :
G.path v u

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

Equations
source
theorem simple_graph.path.count_support_eq_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} {p : G.path u v} (hw : w ∈ ↑p.support) :
list.count w ↑p.support = 1
source
theorem simple_graph.path.count_edges_eq_one {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} {p : G.path u v} (e : sym2 V) (hw : e ∈ ↑p.edges) :
list.count e ↑p.edges = 1
source
@[simp]
theorem simple_graph.path.nodup_support {V : Type u} {G : simple_graph V} {u v : V} (p : G.path u v) :
↑p.support.nodup
source
theorem simple_graph.path.loop_eq {V : Type u} {G : simple_graph V} {v : V} (p : G.path v v) :
p = simple_graph.path.nil
source
theorem simple_graph.path.not_mem_edges_of_loop {V : Type u} {G : simple_graph V} {v : V} {e : sym2 V} {p : G.path v v} :
e ∉ ↑p.edges
source
theorem simple_graph.path.cons_is_cycle {V : Type u} {G : simple_graph V} {u v : V} (p : G.path v u) (h : G.adj u v) (he : ⟦(u, v)⟧ ∉ ↑p.edges) :
(simple_graph.walk.cons h ↑p).is_cycle

Walks to paths #

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

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

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

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

Equations
source
theorem simple_graph.walk.support_bypass_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
p.bypass.support ⊆ p.support
source
theorem simple_graph.walk.support_to_path_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
↑(p.to_path).support ⊆ p.support
source
theorem simple_graph.walk.darts_bypass_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
p.bypass.darts ⊆ p.darts
source
theorem simple_graph.walk.edges_bypass_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
p.bypass.edges ⊆ p.edges
source
theorem simple_graph.walk.darts_to_path_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
↑(p.to_path).darts ⊆ p.darts
source
theorem simple_graph.walk.edges_to_path_subset {V : Type u} {G : simple_graph V} [decidable_eq V] {u v : V} (p : G.walk u v) :
↑(p.to_path).edges ⊆ p.edges

Mapping paths #

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

Given a graph homomorphism, map walks to walks.

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

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

source
@[simp]
theorem simple_graph.walk.map_eq_nil_iff {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u : V} {p : G.walk u u} :
simple_graph.walk.map f p = simple_graph.walk.nil ↔ p = simple_graph.walk.nil
source
@[simp]
theorem simple_graph.walk.length_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
(simple_graph.walk.map f p).length = p.length
source
theorem simple_graph.walk.map_append {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v w : V} (p : G.walk u v) (q : G.walk v w) :
simple_graph.walk.map f (p.append q) = (simple_graph.walk.map f p).append (simple_graph.walk.map f q)
source
@[simp]
theorem simple_graph.walk.reverse_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
(simple_graph.walk.map f p).reverse = simple_graph.walk.map f p.reverse
source
@[simp]
theorem simple_graph.walk.support_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
(simple_graph.walk.map f p).support = list.map ⇑f p.support
source
@[simp]
theorem simple_graph.walk.darts_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
(simple_graph.walk.map f p).darts = list.map f.map_dart p.darts
source
@[simp]
theorem simple_graph.walk.edges_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (p : G.walk u v) :
(simple_graph.walk.map f p).edges = list.map (sym2.map ⇑f) p.edges
source
theorem simple_graph.walk.map_is_path_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u v : V} {p : G.walk u v} (hinj : function.injective ⇑f) (hp : p.is_path) :
(simple_graph.walk.map f p).is_path
source
@[protected]
theorem simple_graph.walk.is_path.of_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {u v : V} {p : G.walk u v} {f : G →g G'} (hp : (simple_graph.walk.map f p).is_path) :
p.is_path
source
theorem simple_graph.walk.map_is_path_iff_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u v : V} {p : G.walk u v} (hinj : function.injective ⇑f) :
(simple_graph.walk.map f p).is_path ↔ p.is_path
source
theorem simple_graph.walk.map_is_trail_iff_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u v : V} {p : G.walk u v} (hinj : function.injective ⇑f) :
(simple_graph.walk.map f p).is_trail ↔ p.is_trail
source
theorem simple_graph.walk.map_is_trail_of_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} {u v : V} {p : G.walk u v} (hinj : function.injective ⇑f) :
p.is_trail → (simple_graph.walk.map f p).is_trail

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Given an injective graph homomorphism, map paths to paths.

Equations
source
theorem simple_graph.path.map_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {f : G →g G'} (hinj : function.injective ⇑f) (u v : V) :
function.injective (simple_graph.path.map f hinj)
source
@[protected]
def simple_graph.path.map_embedding {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G ↪g G') {u v : V} (p : G.path u v) :
G'.path (⇑f u) (⇑f v)

Given a graph embedding, map paths to paths.

Equations
source
@[simp]
theorem simple_graph.path.map_embedding_coe {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G ↪g G') {u v : V} (p : G.path u v) :
↑(simple_graph.path.map_embedding f p) = simple_graph.walk.map f.to_hom ↑p
source
theorem simple_graph.path.map_embedding_injective {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G ↪g G') (u v : V) :
function.injective (simple_graph.path.map_embedding f)

Transferring between graphs #

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

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

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

Deleting edges #

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

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

Equations
source
@[simp]
theorem simple_graph.walk.to_delete_edges_nil {V : Type u} {G : simple_graph V} (s : set (sym2 V)) {v : V} (hp : ∀ (e : sym2 V), e ∈ simple_graph.walk.nil.edges → e ∉ s) :
simple_graph.walk.to_delete_edges s simple_graph.walk.nil hp = simple_graph.walk.nil
source
@[simp]
theorem simple_graph.walk.to_delete_edges_cons {V : Type u} {G : simple_graph V} (s : set (sym2 V)) {u v w : V} (h : G.adj u v) (p : G.walk v w) (hp : ∀ (e : sym2 V), e ∈ (simple_graph.walk.cons h p).edges → e ∉ s) :
simple_graph.walk.to_delete_edges s (simple_graph.walk.cons h p) hp = simple_graph.walk.cons _ (simple_graph.walk.to_delete_edges s p _)
source
@[reducible]
def simple_graph.walk.to_delete_edge {V : Type u} {G : simple_graph V} {v w : V} (e : sym2 V) (p : G.walk v w) (hp : e ∉ p.edges) :
(G.delete_edges {e}).walk v w

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

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

reachable and connected #

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

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

Equations
Instances for simple_graph.reachable
source
theorem simple_graph.reachable_iff_nonempty_univ {V : Type u} {G : simple_graph V} {u v : V} :
G.reachable u v ↔ set.univ.nonempty
source
@[protected]
theorem simple_graph.reachable.elim {V : Type u} {G : simple_graph V} {p : Prop} {u v : V} (h : G.reachable u v) (hp : G.walk u v → p) :
p
source
@[protected]
theorem simple_graph.reachable.elim_path {V : Type u} {G : simple_graph V} {p : Prop} {u v : V} (h : G.reachable u v) (hp : G.path u v → p) :
p
source
@[protected]
theorem simple_graph.walk.reachable {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
G.reachable u v
source
@[protected]
theorem simple_graph.adj.reachable {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
G.reachable u v
source
@[protected, refl]
theorem simple_graph.reachable.refl {V : Type u} {G : simple_graph V} (u : V) :
G.reachable u u
source
@[protected]
theorem simple_graph.reachable.rfl {V : Type u} {G : simple_graph V} {u : V} :
G.reachable u u
source
@[protected, symm]
theorem simple_graph.reachable.symm {V : Type u} {G : simple_graph V} {u v : V} (huv : G.reachable u v) :
G.reachable v u
source
theorem simple_graph.reachable_comm {V : Type u} {G : simple_graph V} {u v : V} :
G.reachable u v ↔ G.reachable v u
source
@[protected, trans]
theorem simple_graph.reachable.trans {V : Type u} {G : simple_graph V} {u v w : V} (huv : G.reachable u v) (hvw : G.reachable v w) :
G.reachable u w
source
theorem simple_graph.reachable_iff_refl_trans_gen {V : Type u} {G : simple_graph V} (u v : V) :
G.reachable u v ↔ relation.refl_trans_gen G.adj u v
source
@[protected]
theorem simple_graph.reachable.map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (f : G →g G') {u v : V} (h : G.reachable u v) :
G'.reachable (⇑f u) (⇑f v)
source
theorem simple_graph.iso.reachable_iff {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {φ : G ≃g G'} {u v : V} :
G'.reachable (⇑φ u) (⇑φ v) ↔ G.reachable u v
source
theorem simple_graph.iso.symm_apply_reachable {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {φ : G ≃g G'} {u : V} {v : V'} :
G.reachable (⇑(φ.symm) v) u ↔ G'.reachable v (⇑φ u)
source
theorem simple_graph.reachable_is_equivalence {V : Type u} (G : simple_graph V) :
equivalence G.reachable
source
def simple_graph.reachable_setoid {V : Type u} (G : simple_graph V) :
setoid V

The equivalence relation on vertices given by simple_graph.reachable.

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

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

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

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

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

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

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

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

Gives the connected component containing a particular vertex.

Equations
source
@[simp]
theorem simple_graph.connected_component.inhabited_default {V : Type u} {G : simple_graph V} [inhabited V] :
inhabited.default = G.connected_component_mk inhabited.default
source
@[protected, instance]
def simple_graph.connected_component.inhabited {V : Type u} {G : simple_graph V} [inhabited V] :
inhabited G.connected_component
Equations
source
@[protected]
theorem simple_graph.connected_component.ind {V : Type u} {G : simple_graph V} {β : G.connected_component → Prop} (h : ∀ (v : V), β (G.connected_component_mk v)) (c : G.connected_component) :
β c
source
@[protected]
theorem simple_graph.connected_component.ind₂ {V : Type u} {G : simple_graph V} {β : G.connected_component → G.connected_component → Prop} (h : ∀ (v w : V), β (G.connected_component_mk v) (G.connected_component_mk w)) (c d : G.connected_component) :
β c d
source
@[protected]
theorem simple_graph.connected_component.sound {V : Type u} {G : simple_graph V} {v w : V} :
G.reachable v w → G.connected_component_mk v = G.connected_component_mk w
source
@[protected]
theorem simple_graph.connected_component.exact {V : Type u} {G : simple_graph V} {v w : V} :
G.connected_component_mk v = G.connected_component_mk w → G.reachable v w
source
@[protected, simp]
theorem simple_graph.connected_component.eq {V : Type u} {G : simple_graph V} {v w : V} :
G.connected_component_mk v = G.connected_component_mk w ↔ G.reachable v w
source
theorem simple_graph.connected_component.connected_component_mk_eq_of_adj {V : Type u} {G : simple_graph V} {v w : V} (a : G.adj v w) :
G.connected_component_mk v = G.connected_component_mk w
source
@[protected]
def simple_graph.connected_component.lift {V : Type u} {G : simple_graph V} {β : Sort u_1} (f : V → β) (h : ∀ (v w : V) (p : G.walk v w), p.is_path → f v = f w) :
G.connected_component → β

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

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

The map on connected components induced by a graph homomorphism.

Equations
source
@[simp]
theorem simple_graph.connected_component.map_mk {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G →g G') (v : V) :
simple_graph.connected_component.map φ (G.connected_component_mk v) = G'.connected_component_mk (⇑φ v)
source
@[simp]
theorem simple_graph.connected_component.map_id {V : Type u} {G : simple_graph V} (C : G.connected_component) :
simple_graph.connected_component.map simple_graph.hom.id C = C
source
@[simp]
theorem simple_graph.connected_component.map_comp {V : Type u} {V' : Type v} {V'' : Type w} {G : simple_graph V} {G' : simple_graph V'} {G'' : simple_graph V''} (C : G.connected_component) (φ : G →g G') (ψ : G' →g G'') :
simple_graph.connected_component.map ψ (simple_graph.connected_component.map φ C) = simple_graph.connected_component.map (ψ.comp φ) C
source
@[simp]
theorem simple_graph.connected_component.iso_image_comp_eq_map_iff_eq_comp {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {φ : G ≃g G'} {v : V} {C : G.connected_component} :
G'.connected_component_mk (⇑φ v) = simple_graph.connected_component.map ↑↑φ C ↔ G.connected_component_mk v = C
source
@[simp]
theorem simple_graph.connected_component.iso_inv_image_comp_eq_iff_eq_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {φ : G ≃g G'} {v' : V'} {C : G.connected_component} :
G.connected_component_mk (⇑(φ.symm) v') = C ↔ G'.connected_component_mk v' = simple_graph.connected_component.map ↑φ C
source
@[simp]
theorem simple_graph.iso.connected_component_equiv_apply {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G ≃g G') (C : G.connected_component) :
⇑(φ.connected_component_equiv) C = simple_graph.connected_component.map ↑φ C
source
@[simp]
theorem simple_graph.iso.connected_component_equiv_symm_apply {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G ≃g G') (C : G'.connected_component) :
⇑(φ.connected_component_equiv.symm) C = simple_graph.connected_component.map ↑(φ.symm) C
source
def simple_graph.iso.connected_component_equiv {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G ≃g G') :
G.connected_component ≃ G'.connected_component

An isomorphism of graphs induces a bijection of connected components.

Equations
source
@[simp]
theorem simple_graph.iso.connected_component_equiv_refl {V : Type u} {G : simple_graph V} :
simple_graph.iso.refl.connected_component_equiv = equiv.refl G.connected_component
source
@[simp]
theorem simple_graph.iso.connected_component_equiv_symm {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G ≃g G') :
φ.symm.connected_component_equiv = φ.connected_component_equiv.symm
source
@[simp]
theorem simple_graph.iso.connected_component_equiv_trans {V : Type u} {V' : Type v} {V'' : Type w} {G : simple_graph V} {G' : simple_graph V'} {G'' : simple_graph V''} (φ : G ≃g G') (φ' : G' ≃g G'') :
simple_graph.iso.connected_component_equiv (rel_iso.trans φ φ') = φ.connected_component_equiv.trans φ'.connected_component_equiv
source
def simple_graph.connected_component.supp {V : Type u} {G : simple_graph V} (C : G.connected_component) :
set V

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

Equations
source
@[ext]
theorem simple_graph.connected_component.supp_injective {V : Type u} {G : simple_graph V} :
function.injective simple_graph.connected_component.supp
source
@[simp]
theorem simple_graph.connected_component.supp_inj {V : Type u} {G : simple_graph V} {C D : G.connected_component} :
C.supp = D.supp ↔ C = D
source
@[protected, instance]
def simple_graph.connected_component.set_like {V : Type u} {G : simple_graph V} :
set_like G.connected_component V
Equations
source
@[simp]
theorem simple_graph.connected_component.mem_supp_iff {V : Type u} {G : simple_graph V} (C : G.connected_component) (v : V) :
v ∈ C.supp ↔ G.connected_component_mk v = C
source
theorem simple_graph.connected_component.connected_component_mk_mem {V : Type u} {G : simple_graph V} {v : V} :
v ∈ G.connected_component_mk v
source
def simple_graph.connected_component.iso_equiv_supp {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} (φ : G ≃g G') (C : G.connected_component) :
↥(C.supp) ≃ ↥((⇑(φ.connected_component_equiv) C).supp)

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

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

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

source
theorem simple_graph.singleton_subgraph_connected {V : Type u} {G : simple_graph V} {v : V} :
(G.singleton_subgraph v).connected
source
@[simp]
theorem simple_graph.subgraph_of_adj_connected {V : Type u} {G : simple_graph V} {v w : V} (hvw : G.adj v w) :
(G.subgraph_of_adj hvw).connected
source
theorem simple_graph.preconnected.set_univ_walk_nonempty {V : Type u} {G : simple_graph V} (hconn : G.preconnected) (u v : V) :
set.univ.nonempty
source
theorem simple_graph.connected.set_univ_walk_nonempty {V : Type u} {G : simple_graph V} (hconn : G.connected) (u v : V) :
set.univ.nonempty

Walks as subgraphs #

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

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

Equations
source
theorem simple_graph.walk.to_subgraph_cons_nil_eq_subgraph_of_adj {V : Type u} {G : simple_graph V} {u v : V} (h : G.adj u v) :
(simple_graph.walk.cons h simple_graph.walk.nil).to_subgraph = G.subgraph_of_adj h
source
theorem simple_graph.walk.mem_verts_to_subgraph {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) :
w ∈ p.to_subgraph.verts ↔ w ∈ p.support
source
@[simp]
theorem simple_graph.walk.verts_to_subgraph {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.to_subgraph.verts = {w : V | w ∈ p.support}
source
theorem simple_graph.walk.mem_edges_to_subgraph {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) {e : sym2 V} :
e ∈ p.to_subgraph.edge_set ↔ e ∈ p.edges
source
@[simp]
theorem simple_graph.walk.edge_set_to_subgraph {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.to_subgraph.edge_set = {e : sym2 V | e ∈ p.edges}
source
@[simp]
theorem simple_graph.walk.to_subgraph_append {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) (q : G.walk v w) :
(p.append q).to_subgraph = p.to_subgraph ⊔ q.to_subgraph
source
@[simp]
theorem simple_graph.walk.to_subgraph_reverse {V : Type u} {G : simple_graph V} {u v : V} (p : G.walk u v) :
p.reverse.to_subgraph = p.to_subgraph
source
@[simp]
theorem simple_graph.walk.to_subgraph_rotate {V : Type u} {G : simple_graph V} {u v : V} [decidable_eq V] (c : G.walk v v) (h : u ∈ c.support) :
(c.rotate h).to_subgraph = c.to_subgraph
source
@[simp]
theorem simple_graph.walk.to_subgraph_map {V : Type u} {V' : Type v} {G : simple_graph V} {G' : simple_graph V'} {u v : V} (f : G →g G') (p : G.walk u v) :
(simple_graph.walk.map f p).to_subgraph = simple_graph.subgraph.map f p.to_subgraph
source
@[simp]
theorem simple_graph.walk.finite_neighbor_set_to_subgraph {V : Type u} {G : simple_graph V} {u v w : V} (p : G.walk u v) :
(p.to_subgraph.neighbor_set w).finite

Walks of a given length #

source
theorem simple_graph.set_walk_self_length_zero_eq {V : Type u} {G : simple_graph V} (u : V) :
{p : G.walk u u | p.length = 0} = {simple_graph.walk.nil}
source
theorem simple_graph.set_walk_length_zero_eq_of_ne {V : Type u} {G : simple_graph V} {u v : V} (h : u ≠ v) :
{p : G.walk u v | p.length = 0} = ∅
source
theorem simple_graph.set_walk_length_succ_eq {V : Type u} {G : simple_graph V} (u v : V) (n : ℕ) :
{p : G.walk u v | p.length = n.succ} = ⋃ (w : V) (h : G.adj u w), simple_graph.walk.cons h '' {p' : G.walk w v | p'.length = n}
source
def simple_graph.finset_walk_length {V : Type u} (G : simple_graph V) [decidable_eq V] [G.locally_finite] (n : ℕ) (u v : V) :
finset (G.walk u v)

The finset of length-n walks from u to v. This is used to give {p : G.walk u v | p.length = n} a fintype instance, and it can also be useful as a recursive description of this set when V is finite.

See simple_graph.coe_finset_walk_length_eq for the relationship between this finset and the set of length-n walks.

Equations
source
theorem simple_graph.coe_finset_walk_length_eq {V : Type u} (G : simple_graph V) [decidable_eq V] [G.locally_finite] (n : ℕ) (u v : V) :
↑(G.finset_walk_length n u v) = {p : G.walk u v | p.length = n}
source
theorem simple_graph.walk.mem_finset_walk_length_iff_length_eq {V : Type u} {G : simple_graph V} [decidable_eq V] [G.locally_finite] {n : ℕ} {u v : V} (p : G.walk u v) :
p ∈ G.finset_walk_length n u v ↔ p.length = n
source
@[protected, instance]
def simple_graph.fintype_set_walk_length {V : Type u} (G : simple_graph V) [decidable_eq V] [G.locally_finite] (u v : V) (n : ℕ) :
fintype ↥{p : G.walk u v | p.length = n}
Equations
source
theorem simple_graph.set_walk_length_to_finset_eq {V : Type u} (G : simple_graph V) [decidable_eq V] [G.locally_finite] (n : ℕ) (u v : V) :
{p : G.walk u v | p.length = n}.to_finset = G.finset_walk_length n u v
source
theorem simple_graph.card_set_walk_length_eq {V : Type u} (G : simple_graph V) [decidable_eq V] [G.locally_finite] (u v : V) (n : ℕ) :
fintype.card ↥{p : G.walk u v | p.length = n} = (G.finset_walk_length n u v).card
source
@[protected, instance]
def simple_graph.fintype_set_path_length {V : Type u} (G : simple_graph V) [decidable_eq V] [G.locally_finite] (u v : V) (n : ℕ) :
fintype ↥{p : G.walk u v | p.is_path ∧ p.length = n}
Equations
source
theorem simple_graph.reachable_iff_exists_finset_walk_length_nonempty {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] (u v : V) :
G.reachable u v ↔ ∃ (n : fin (fintype.card V)), (G.finset_walk_length ↑n u v).nonempty
source
@[protected, instance]
def simple_graph.reachable.decidable_rel {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] :
decidable_rel G.reachable
Equations
source
@[protected, instance]
def simple_graph.connected_component.fintype {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] :
fintype G.connected_component
Equations
source
@[protected, instance]
def simple_graph.preconnected.decidable {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] :
decidable G.preconnected
Equations
source
@[protected, instance]
def simple_graph.connected.decidable {V : Type u} (G : simple_graph V) [decidable_eq V] [fintype V] [decidable_rel G.adj] :
decidable G.connected
Equations

Bridge edges #

source
def simple_graph.is_bridge {V : Type u} (G : simple_graph V) (e : sym2 V) :
Prop

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

Equations
source
theorem simple_graph.is_bridge_iff {V : Type u} {G : simple_graph V} {u v : V} :
G.is_bridge ⟦(u, v)⟧ ↔ G.adj u v ∧ ¬(G \ simple_graph.from_edge_set {⟦(u, v)⟧}).reachable u v
source
theorem simple_graph.reachable_delete_edges_iff_exists_walk {V : Type u} {G : simple_graph V} {v w : V} :
(G \ simple_graph.from_edge_set {⟦(v, w)⟧}).reachable v w ↔ ∃ (p : G.walk v w), ⟦(v, w)⟧ ∉ p.edges
source
theorem simple_graph.is_bridge_iff_adj_and_forall_walk_mem_edges {V : Type u} {G : simple_graph V} {v w : V} :
G.is_bridge ⟦(v, w)⟧ ↔ G.adj v w ∧ ∀ (p : G.walk v w), ⟦(v, w)⟧ ∈ p.edges
source
theorem simple_graph.reachable_delete_edges_iff_exists_cycle.aux {V : Type u} {G : simple_graph V} [decidable_eq V] {u v w : V} (hb : ∀ (p : G.walk v w), ⟦(v, w)⟧ ∈ p.edges) (c : G.walk u u) (hc : c.is_trail) (he : ⟦(v, w)⟧ ∈ c.edges) (hw : w ∈ (c.take_until v _).support) :
false
source
theorem simple_graph.adj_and_reachable_delete_edges_iff_exists_cycle {V : Type u} {G : simple_graph V} {v w : V} :
G.adj v w ∧ (G \ simple_graph.from_edge_set {⟦(v, w)⟧}).reachable v w ↔ ∃ (u : V) (p : G.walk u u), p.is_cycle ∧ ⟦(v, w)⟧ ∈ p.edges
source
theorem simple_graph.is_bridge_iff_adj_and_forall_cycle_not_mem {V : Type u} {G : simple_graph V} {v w : V} :
G.is_bridge ⟦(v, w)⟧ ↔ G.adj v w ∧ ∀ ⦃u : V⦄ (p : G.walk u u), p.is_cycle → ⟦(v, w)⟧ ∉ p.edges
source
theorem simple_graph.is_bridge_iff_mem_and_forall_cycle_not_mem {V : Type u} {G : simple_graph V} {e : sym2 V} :
G.is_bridge e ↔ e ∈ ⇑simple_graph.edge_set G ∧ ∀ ⦃u : V⦄ (p : G.walk u u), p.is_cycle → e ∉ p.edges