Trail, Path, and Cycle

In a simple graph,

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

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

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

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

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

Main definitions

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

• SimpleGraph.Path

• SimpleGraph.Path.map for the induced map on paths, 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

trails, paths, circuits, cycles, bridge edges

Trails, paths, circuits, cycles

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

A trail is a walk with no repeating edges.

• edges_nodup : p.edges.Nodup

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

theorem SimpleGraph.Walk.IsTrail.length_le_card_edgeFinset {V : Type u} {G : SimpleGraph V} [Fintype ↑G.edgeSet] {u v : V} {w : G.Walk u v} (h : w.IsTrail) : w.length ≤ G.edgeFinset.card

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

About paths

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

Equations

• p.instDecidableIsPathOfDecidableEq = ⋯.mpr inferInstance

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

Walk decompositions

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

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

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

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

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

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

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

Type of paths

@[reducible, inline]

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

The type for paths between two vertices.

Equations

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

@[simp]

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

@[simp]

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

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

The length-0 path at a vertex.

Equations

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

@[simp]

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

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

@[simp]

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

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

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

@[simp]

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

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

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

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

Walks to paths

def SimpleGraph.Walk.bypass {V : Type u} {G : SimpleGraph V} [DecidableEq V] {u v : V} : G.Walk u v → G.Walk u v

Given a walk, produces a walk from it by bypassing subwalks between repeated vertices. The result is a path, as shown in SimpleGraph.Walk.bypass_isPath. This is packaged up in SimpleGraph.Walk.toPath.

Equations

• SimpleGraph.Walk.nil.bypass = SimpleGraph.Walk.nil
• (SimpleGraph.Walk.cons ha p).bypass = if hs : u ∈ p.bypass.support then p.bypass.dropUntil u hs else SimpleGraph.Walk.cons ha p.bypass

@[simp]

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

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

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

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

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

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

Equations

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

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

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

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

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

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

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

Mapping paths

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

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

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

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

Given an injective graph homomorphism, map paths to paths.

Equations

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

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

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

def SimpleGraph.Path.mapEmbedding {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph 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

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

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

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

Transferring between graphs

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

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

Deleting edges

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

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

@[simp]

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

Reachable and Connected

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem SimpleGraph.reachable_bot {V : Type u} {u v : V} : ⊥.Reachable u v ↔ u = v

Distinct vertices are not reachable in the empty graph.

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

The equivalence relation on vertices given by SimpleGraph.Reachable.

Equations

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

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

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

Equations

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

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

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

theorem SimpleGraph.bot_preconnected_iff_subsingleton {V : Type u} : ⊥.Preconnected ↔ Subsingleton V

theorem SimpleGraph.bot_preconnected {V : Type u} [Subsingleton V] : ⊥.Preconnected

theorem SimpleGraph.bot_not_preconnected {V : Type u} [Nontrivial V] : ¬⊥.Preconnected

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

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

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

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

There is a CoeFun instance so that h u v can be used instead of h.Preconnected u v.

• preconnected : G.Preconnected
• nonempty : Nonempty V

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

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

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

Equations

• G.instCoeFunConnectedForallForallReachable = { coe := ⋯ }

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

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

theorem SimpleGraph.bot_not_connected {V : Type u} [Nontrivial V] : ¬⊥.Connected

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

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

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

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

Equations

• G.ConnectedComponent = Quot G.Reachable

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

Gives the connected component containing a particular vertex.

Equations

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

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

Equations

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

@[simp]

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

instance SimpleGraph.ConnectedComponent.isEmpty {V : Type u} {G : SimpleGraph V} [IsEmpty V] : IsEmpty G.ConnectedComponent

Equations

• ⋯ = ⋯

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

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

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

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

@[simp]

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

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

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

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

Equations

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

@[simp]

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

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

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

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

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

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

Equations

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

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

The map on connected components induced by a graph homomorphism.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

An isomorphism of graphs induces a bijection of connected components.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

@[simp]

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

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

Equations

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

@[simp]

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

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

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

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

Equations

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

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

theorem SimpleGraph.ConnectedComponent.connectedComponentMk_supp_subset_supp {V : Type u} {G G' : SimpleGraph V} {v : V} (h : G ≤ G') (c' : G'.ConnectedComponent) (hc' : v ∈ c'.supp) : (G.connectedComponentMk v).supp ⊆ c'.supp

theorem SimpleGraph.ConnectedComponent.biUnion_supp_eq_supp {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') (c' : G'.ConnectedComponent) : ⋃ (c : G.ConnectedComponent), ⋃ (_ : c.supp ⊆ c'.supp), c.supp = c'.supp

theorem SimpleGraph.ConnectedComponent.top_supp_eq_univ {V : Type u} (c : ⊤.ConnectedComponent) : c.supp = Set.univ

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

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

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

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

Bridge edges

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

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

Equations

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

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

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

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

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

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

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

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